DPOP

A DPOP implementation for solving DCOP problems.

It uses a simple textual input format, initially developed for describing Multi Robot Patrolling instances, but quite general to be used for any distributed constraint optimization problem.

The program can be started using the script dpop or executing the JAR file directly.
 

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

A set of linear test instances.

A set of grid test instances.

JavaCC in 30 minuti

Già sapete che JavaCC è un generatore di parser/analizzatori lessicali, quindi passiamo oltre.


1. Create dunque una directory, esempio javacctut
2. Scaricate JavaCC da http://javacc.java.net/ e scompattate l’archivio - il programma che useremo è bin/javacc
3. Aprite il vostro editor di testi (o IDE Java) preferito


Ora dobbiamo creare un file di testo con estensione jj che specifica la grammatica del linguaggio che vogliamo riconoscere - chiamiamolo ftp.jj.
In questo tutorial genereremo un parser per un semplice linguaggio di specifica di alberi genealogici, che accetta in ingresso un file formato come il seguente:


ada.padre = pino
ada.madre = rina

ugo.padre = pino
ugo.madre = tina

ida.padre = pino
ida.madre = lina

edo.padre = pino
edo.madre = mina

leo.padre = pino
leo.madre = gina

# eh, si', pino si e' dato da fare...

pino.madre = dina
pino.padre = mario

in cui una dichiarazione del tipo ada.padre = pino significa ovviamente che pino è il padre di ada (usiamo lettere minuscole per semplicità).
Chiamiamo inoltre generazione una dichiarazione siffatta.
Apriamo allora questo file ftp.jj e inseriamo il seguente codice:

PARSER_BEGIN(FamilyTreeParser)
package javacctut;
public class FamilyTreeParser {
}
PARSER_END(FamilyTreeParser)

nel quale mettiamo il nome del parser ed eventuale altro codice java (come importazioni e dichiarazione del package).
Adesso bisogna dire a JavaCC cosa ignorare:

SKIP:
{
<" " | "\n" | "\r" | "\t">
| <"#"(~["\n"])* "\n"> // comment
}

ovvero whitespaces e commenti (qualsiasi stringa che inizia con “#”). Notate che “// comment” è un commento alla riga inserita in ftp.jj, e non fa parte della grammatica (verrà ignorato nella generazione del parser).

Ora dichiariamo le sequenze di caratteri da riconoscere:

TOKEN:
{
<FATHER: "padre" | "father">
| <MOTHER: "madre" | "mother">
| <NAME: (["a"-"z"])+>
| <DOT: ".">
| <EQUALS: "=">
}

Ci servono token che specificano padre o madre (notate in OR le versioni in inglese), nomi di persona (uno o più lettere minuscole), il punto e il simbolo di uguale.
L’ordine dei token è importante, in quanto in caso di ambiguità nel riconoscimento di una stringa viene scelta la regola che viene prima (ad esempio “madre” viene considerato di tipo MOTHER e non di tipo NAME).

In seguito si devono inserire le produzioni della grammatica che stabiliscono la struttura del nostro “albero genealogico”. La prima ci dice che il file è una sequenza di zero o più “generazioni”:

void Start():
{}
{
    ( Generation() )*
}

Una generazione ha invece la struttura che segue:

void Generation():
{}
{
    <NAME> <DOT> ( <FATHER> | <MOTHER> ) <EQUALS> <NAME>
}

ovvero un token NAME seguito da punto, padre o madre, uguale, e un altro token di tipo NAME.

Eseguendo il comando
javacc -STATIC=false ftp.jj
vengono prodotti dei sorgenti java che implementano il parser.
Nota: l’opzione -STATIC=false dice a JavaCC di generare metodi non statici. Questa opzione può anche essere specificata in testa al file della grammatica con options { STATIC = false; }.

La scansione del file viene fatta con il codice:

java.io.Reader infile = new java.io.FileReader(nomeFile);
FamilyTreeParser parser = new FamilyTreeParser(infile);
parser.Start();

che può essere messo in una classe separata o direttamente in un metodo main tra PARSER_BEGIN e PARSER_END.
nomeFile è il nome del file contenente l’albero genealogico - può essere args[0] in un metodo main.

Non resta che compilare tutti i sorgenti ed eseguire il codice sopra su un file ben formato, come l’esempio di pino. Non dovrebbe venir stampato niente - mentre dovrebbe essere segnalato errore se viene trovata una virgola al posto di un punto, ad esempio.
Se a javacc passiamo l’opzione -debug_parser vengono invece stampati i token e le produzioni riconosciuti.

Generazione dell’albero in formato DOT

Se avete ancora un po’ di tempo vi mostro come generare la rappresentazione grafica dell’albero genealogico con piccole modifiche al file jj.
In pratica effettueremo una traduzione della specifica dell’albero in formato DOT, leggibile dal programma dot, della suite Graphviz (apt install graphviz, o vedi http://graphviz.org/).
Un esempio di un semplice grafo con due vertici e un arco è
digraph {
a -> b
}
e, assumendo che sia contenuto nel file g.dot, si può produrre un file PDF con
dot -Tpdf g.dot -o g.pdf
(sono disponibili altri formati, si veda la documentazione di dot).

Inseriremo nella classe del parser un metodo getDOT() che restituisce una stringa contenente il grafo in formato DOT, pronto per essere compilato come sopra.
Per prima cosa modifichiamo la sezione del parser in questo modo (in rosso le parti nuove):

PARSER_BEGIN(FamilyTreeParser)
package javacctut;

public class FamilyTreeParser {
    private StringBuilder sb = new StringBuilder("digraph {\n");

    public String getDOT() {
           return sb.append("}\n").toString();
    }
}
PARSER_END(FamilyTreeParser)

per inserire un campo di tipo StringBuilder, che verrà aggiornato a ogni generazione con l’arco corrispondente, e il metodo getDOT().

Poi la produzione Generation:

void Generation():
{
    Token child, parent;
}
{
    child = <NAME> <DOT> ( <FATHER> | <MOTHER> ) <EQUALS> parent = <NAME>
    { sb.append(parent.image).append(" -> ") .append(child.image).append("\n"); }
}

Ho aggiunto la dichiarazione di due Token, child e parent, che servono a memorizzare i due nomi, e una riga di codice java che aggiunge un arco allo StringBuilder (il campo image di Token è semplicemente la rappresentazione testuale del token).

Le parti aggiunte vengono copiate nel codice sorgente del parser così come sono (quasi).

Dopo il parsing possiamo quindi stampare su schermo (o salvare su file) il grafo prodotto:

java.io.Reader infile = new java.io.FileReader(nomeFile);
FamilyTreeParser parser = new FamilyTreeParser(infile);
parser.Start();
System.out.println(parser.getDOT());

Se provate adesso a processare la famiglia di pino produrrete il grafo seguente

In questo caso il parsing ha prodotto una stringa, ma naturalmente si possono creare strutture più complesse (grafi, alberi, liste, ecc.)


Buona codifica!

TeePee, a theorem prover

TeePee is a simple theorem prover for CNF FOL formulae.
It doesn't aim to be a fully featured prover (like Prover9, E and others) but rather an "educational toy", to show a simple implementation of concepts practically used in automated reasoning (being written in one week for a course assignment).

Many things can be improved - for example, ProcessorTest needs a lot of refactoring.

The program can be started using the script teepee or executing the JAR file directly.

Note: on page 4 of the article the problems PLA001-1.p, PLA002-1.p and PLA003-1.p are reported to be satisfiable, which is wrong! I think that's because I considered only clauses marked as "negated conjecture" to belong to the set of support - indeed not using the set-of-support strategy (not using the -sos flag) correctly reports "unsatisfiable".

 

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

Satisfiability in the theory of lists

In this post I will present a program for checking the satisfiability of formulae in the list theory, that I developed as a project for a course in program verification.
For example the formula

atom(x) ^ x=cons(y,z)

is clearly unsatisfiable - here "^" means "AND".

It uses the Nelson-Oppen congruence closure algorithm, as described in this book and in this article.
The only requirement is a Java Runtime Environment.

Under UNIX the program can be started with ./listsat. You'll see that the program complains for missing options. If you pass the name of a (well formed) file containing a formula it prints something like:

Loading formula from file: ../random/r3.txt
Loaded after 0.265 secs

Formula contains 95 positive literals, 48 negative literals, 57 atoms (200 total).
Constructing initial DAG...
DAG constructed - time: 0.093
DAG has 921 nodes.
Starting Congruence Closure algorithm...

 ========== ========== ========== ========== ========== ========== [60/200]
 ========== ========== ========== =====*

CC algorithm ended - time: 0.685

Formula is UNSATISFIABLE
Last processed literal: g(h(x,y,f(x,t(x))),f(z,g(y,y)))!=y.



If you want to start the graphical interface pass the option -g.

The ListSAT main window

Here you can generate a random formula

The dialog for running the benchmarks.

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

Sicurezza delle Smart Card

Una Smart Card! (da Wikipedia)

An overview (in Italian) of Smart Cards’ Security. It covers power analysis as well as other physical attacks that can break the security of secrets stored in the card.  Of course nothing in this material is original, since it was a course assignment - see the bibliography at pages 15-16.

Oggi pubblico un articolo sulla sicurezza delle smart card, quelle tesserine che abbiamo tutti, in tasca o nel telefono cellulare .
Nell’articolo non troverete niente di originale, visto che è un progetto d’esame,
serve più che altro a introdurre le varie modalità di  attacco ai segreti memorizzati su questi dispositivi, a cui evidentemente i progettisti delle prime smart card non avevano pensato.

Articolo 

Presentazione 

Buona lettura!