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