Commit 9b28838d authored by Maximilien Colange's avatar Maximilien Colange

Add new tests.

parent 7c787430
...@@ -51,4 +51,10 @@ TESTS = \ ...@@ -51,4 +51,10 @@ TESTS = \
tests/test_9.data \ tests/test_9.data \
tests/test_10.data \ tests/test_10.data \
tests/test_11.data \ tests/test_11.data \
tests/test_12.data tests/test_12.data \
tests/test_13.data \
tests/test_14.data \
tests/test_15.data \
tests/test_16.data \
tests/test_17.data \
tests/test_18.data
Energy Task Scheduling model, simple reachability, BFS, simple inclusion test
./tiamo reach tests/ets.xml -cora -order BFS -incl simple
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
discrete states: 55
states seen: 249
states explored: 209
max size of storage: 226
incl tests: 1791
pos. incl tests: 179
Result of verification is Reachable!
Path is
Energy Task Scheduling model, simple reachability, BFS, abstract inclusion test
./tiamo reach tests/ets.xml -cora -order BFS -incl sri
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
discrete states: 55
states seen: 68
states explored: 64
max size of storage: 65
incl tests: 74
pos. incl tests: 51
Result of verification is Reachable!
Path is
Energy Task Scheduling model, optimal reachability, BFS, simple inclusion test
./tiamo optimal tests/ets.xml -cora -order BFS -incl simple
[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 1370 replaces 1073741823, found after seeing 525 states
corresponding path has length 13
new optimal value 1350 replaces 1370, found after seeing 526 states
corresponding path has length 13
new optimal value 1340 replaces 1350, found after seeing 527 states
corresponding path has length 13
new optimal value 1320 replaces 1340, found after seeing 528 states
corresponding path has length 13
discrete states: 55
states seen: 638
states explored: 572
max size of storage: 583
incl tests: 15727
pos. incl tests: 340
Result of verification is 1320
Path is
Energy Task Scheduling model, optimal reachability, BFS, abstract inclusion test
./tiamo optimal tests/ets.xml -cora -order BFS -incl exp
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 1340 replaces 1073741823, found after seeing 79 states
corresponding path has length 13
new optimal value 1320 replaces 1340, found after seeing 79 states
corresponding path has length 13
discrete states: 55
states seen: 94
states explored: 80
max size of storage: 80
incl tests: 141
pos. incl tests: 58
Result of verification is 1320
Path is
Energy Task Scheduling model, optimal reachability, SBFS, simple inclusion test
./tiamo optimal tests/ets.xml -cora -order SBFS -incl simple
[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 1320 replaces 1073741823, found after seeing 497 states
corresponding path has length 13
discrete states: 55
states seen: 654
states explored: 654
max size of storage: 582
incl tests: 18144
pos. incl tests: 462
Result of verification is 1320
Path is
Energy Task Scheduling model, optimal reachability, SBFS, abstract inclusion test
./tiamo optimal tests/ets.xml -cora -order SBFS -incl exp
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 1320 replaces 1073741823, found after seeing 81 states
corresponding path has length 13
discrete states: 55
states seen: 107
states explored: 85
max size of storage: 83
incl tests: 174
pos. incl tests: 66
Result of verification is 1320
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