Commit 0850e631 authored by Maximilien Colange's avatar Maximilien Colange

Fix nominal statistical values in tests.

parent 419b5e22
......@@ -3,16 +3,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, abstract inclusio
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
new optimal value 90 replaces 1073741823, found after seeing 1202 states
corresponding path has length 20
cleaning: shrink from 2866 states to 554 states stored
still 1931 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
discrete states: 434
states seen: 3290
states explored: 1202
max size of storage: 2881
incl tests: 60046
pos. incl tests: 3089
Result of verification is 90
Path is
......@@ -2,17 +2,17 @@ Vehicule Routing model, optimal reachability, BBFS cost, abstract inclusion test
./tiamo optimal tests/vrptw.xml -cora -order BBFS -best cost -incl exp -p
Input automaton parsed, computing LU bounds
Took 175 seconds to compute LU bounds
new optimal value 18372 replaces 1073741823, found after seeing 135092 states
Took 0 seconds to compute LU bounds
new optimal value 18372 replaces 1073741823, found after seeing 136922 states
corresponding path has length 27
cleaning: shrink from 144191 states to 135017 states stored
still 9570 states waiting for treatment
cleaning: shrink from 146051 states to 136847 states stored
still 9600 states waiting for treatment
discrete states: 29853
states seen: 151502
states explored: 135092
max size of storage: 144419
incl tests: 1486881
pos. incl tests: 24875
states seen: 153382
states explored: 136922
max size of storage: 146279
incl tests: 1549095
pos. incl tests: 24617
Result of verification is 18372
Path is
......@@ -2,11 +2,12 @@ Fischer model, reachability, BFS, abstract inclusion test
./tiamo reach tests/fischer.xml -incl sri
Input automaton parsed, computing LU bounds
we have explored 200000 states, 530 in the waiting listtt
Took 0 seconds to compute LU bounds
we have explored 220000 states, 3903 in the waiting listt
discrete states: 7737
states seen: 200530
states explored: 200530
max size of storage: 200530
incl tests: 85510147
states seen: 223903
states explored: 223903
max size of storage: 223903
incl tests: 109940539
pos. incl tests: 483595
Result of verification is Not reachable...
......@@ -2,11 +2,12 @@ Fischer model, reachability, DFS, abstract inclusion test
./tiamo reach tests/fischer.xml -order DFS -incl sri
Input automaton parsed, computing LU bounds
we have explored 255000 states, 14 in the waiting listtt
Took 0 seconds to compute LU bounds
we have explored 275000 states, 14 in the waiting listtt
discrete states: 7737
states seen: 258725
states explored: 258688
max size of storage: 200530
incl tests: 112802714
pos. incl tests: 661849
states seen: 279454
states explored: 279454
max size of storage: 223903
incl tests: 138320181
pos. incl tests: 659242
Result of verification is Not reachable...
......@@ -4,16 +4,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, simple inclusion
[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
new optimal value 90 replaces 1073741823, found after seeing 2330 states
corresponding path has length 20
cleaning: shrink from 5703 states to 910 states stored
still 3630 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
discrete states: 434
states seen: 6057
states explored: 2330
max size of storage: 5712
incl tests: 374896
pos. incl tests: 3854
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