Commit d2de471c authored by Maximilien Colange's avatar Maximilien Colange

Add more tests.

parent 0a58952a
......@@ -45,4 +45,8 @@ TESTS = \
tests/test_3.data \
tests/test_4.data \
tests/test_5.data \
tests/test_6.data
tests/test_6.data \
tests/test_7.data \
tests/test_8.data \
tests/test_9.data \
tests/test_10.data
Aicraft Landing System model, optimal reachability, BBFS cost, abstract inclusion test, with pruning
./tiamo optimal tests/als.xml -cora -order BBFS -best cost -incl exp -p
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 90 replaces 1073741823, found after seeing 826 states
corresponding path has length 14
cleaning: shrink from 1837 states to 410 states stored
still 1161 states waiting for treatment
discrete states: 272
states seen: 2081
states explored: 826
max size of storage: 1846
incl tests: 41882
pos. incl tests: 1732
Result of verification is 90
Path is
Aicraft Landing System model, reachability, BFS, simple inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl simple
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
we have explored 285000 states, 10152 in the waiting listt
discrete states: 1736
states seen: 376461
states explored: 285190
max size of storage: 317837
incl tests: 1208691736
pos. incl tests: 1215266
Result of verification is Reachable!
Path is
Aicraft Landing System model, reachability, BFS, abstract inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl sri
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
we have explored 5000 states, 3000 in the waiting list
discrete states: 1736
states seen: 15918
states explored: 9722
max size of storage: 10087
incl tests: 433035
pos. incl tests: 47330
Result of verification is Reachable!
Path is
Aicraft Landing System model, optimal reachability, BBFS cost, simple inclusion test, with pruning
./tiamo optimal tests/als.xml -cora -order BBFS -best cost -incl simple -p
[WARNING] If your automaton is not acyclic or bounded, the chosen inclusion test does not guarantee termination.
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 90 replaces 1073741823, found after seeing 1186 states
corresponding path has length 14
cleaning: shrink from 2879 states to 436 states stored
still 1841 states waiting for treatment
discrete states: 272
states seen: 3085
states explored: 1186
max size of storage: 2887
incl tests: 138544
pos. incl tests: 1540
Result of verification is 90
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