Commit f31aabdb authored by Maximilien Colange's avatar Maximilien Colange

Add tests.

parent d3f46391
......@@ -39,4 +39,7 @@ DATA_LOG_DRIVER = ./teamcity-test-driver
DATA_LOG_COMPILER = ./run_test.pl
TESTS = \
tests/test_1.data
tests/test_1.data \
tests/test_2.data \
tests/test_3.data \
tests/test_4.data
Simple Reachability, default options
Dummy model, reachability, BFS, regular inclusion test
./tiamo reach tests/bla.xml
Input automaton parsed, computing LU bounds
......
Dummy model, reachability, BFS, abstract inclusion test
./tiamo reach tests/bla.xml -incl sri
Input automaton parsed, computing LU bounds
discrete states: 2
states seen: 2
states explored: 1
max size of storage: 2
incl tests: 0
pos. incl tests: 0
Result of verification is Reachable!
Path is
Dummy model, reachability, DFS, regular inclusion test
./tiamo reach tests/bla.xml -order DFS
Input automaton parsed, computing LU bounds
discrete states: 2
states seen: 2
states explored: 1
max size of storage: 2
incl tests: 0
pos. incl tests: 0
Result of verification is Reachable!
Path is
Dummy model, reachability, DFS, abstract inclusion test
./tiamo reach tests/bla.xml -order DFS -incl sri
Input automaton parsed, computing LU bounds
discrete states: 2
states seen: 2
states explored: 1
max size of storage: 2
incl tests: 0
pos. incl tests: 0
Result of verification is Reachable!
Path is
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment