|
THE EXECUTABLE FILES AND SOURCE CODE
The program is implemented in Java and compiled for environment compatible with Sun's JRE with version ≥ 1.6.
It has been tested on OpenJDK 64-Bit Server VM and Java HotSpot(TM) 64-Bit Server VM.
The source code is available here. Usage:
java -jar CheckingInclusion_SimulationSubsumption.jar Aut1_file Aut2_file [-h -q -qr -c -l -rd -DFS -SFS -fplus -b -d -v]
-h: print help page
-q: do quotienting w.r.t. forward simulation
-qr: do fw/bw quotienting repeatedly until a fixed point is reached
-c: use forward simulation between A and B
-l: use layered arc sets
-rd: remove dead states
-DFS: use DFS searching strategy (default: BFS strategy)
-SFS: use smallest-first searching strategy (default: BFS strategy)
-fplus: use one-step-further forward simulation
-b: use backward simulation
-d: debug mode
-v: verbose mode
For best performance we recommend options -q -b -rd -fplus -SFS -qr -c -l
The program will test if L(Aut1) ⊆ L(Aut2), where Aut1 and Aut2 are two Buchi automata described by BA files.
Example:
java -jar CheckingInclusion_SimulationSubsumption.jar peterson.1.ba peterson.1.1.ba -q -rd -fplus -l
Program output:
Ver. 1.10, Test if L(A) <= L(B)
Aut A: # of Trans. 33, # of States 20.
Aut B: # of Trans. 33, # of States 20.
Aut A (dead states removed): # of Trans. 29, # of States 18.
Aut B (dead states removed): # of Trans. 29, # of States 18.
Included
Metagraphs added to the Next set 348
Time for the Simulation Subsumption algorithm(ms): 1232.
BUCHI AUTOMATA MODELS AND THE LOG FILES The automata we used in the first experiment (from real models) are listed below. They are obtained by the following steps:
Forward Simulation Holds Between Initial StatesInclusion Holds, but Forward Simulation Does Not Hold Between Initial States
Inclusion Does Not HoldThe log files and the automata of the second experiment (Tabakov-Vardi Random Model) are listed below. Tabakov-Vardi Model
| ||||||||||||||||||||||||||||||||||||||||||||
|
REFERENCES
|