Commit 709e0e4e authored by Maximilien Colange's avatar Maximilien Colange

Restore the original aircraft landing system from CORA.

Change tests accordingly.
parent b8618979
//This file was generated from UPPAAL CORA 041109, Nov 2004
/*
*/
E<> KL101.done and KL108.done and KL115.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done and KL157.done and KL164.done
...@@ -99,10 +99,10 @@ KL143 = Flight(124,138,577,30,30,0,1); ...@@ -99,10 +99,10 @@ KL143 = Flight(124,138,577,30,30,0,1);
KL150 = Flight(126,140,573,30,30,0,1); KL150 = Flight(126,140,573,30,30,0,1);
KL157 = Flight(135,150,591,30,30,0,1); KL157 = Flight(135,150,591,30,30,0,1);
KL164 = Flight(160,180,657,30,30,0,1); KL164 = Flight(160,180,657,30,30,0,1);
</instantiation><system>system runway0, runway1, KL101, KL108, KL122, KL129, KL136, KL143, KL150;</system> </instantiation><system>system runway0, runway1, KL101, KL108, KL115, KL122, KL129, KL136, KL143, KL150, KL157, KL164;</system>
<queries> <queries>
<query> <query>
<formula>E&lt;&gt; (KL101.done and KL108.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done) <formula>E&lt;&gt; (KL101.done and KL108.done and KL115.done and KL122.done and KL129.done and KL136.done and KL143.done and KL150.done and KL157.done and KL164.done)
</formula> </formula>
<comment> <comment>
</comment> </comment>
......
Aicraft Landing System model, reachability, BFS, simple inclusion test Aicraft Landing System model, reachability, DFS, simple inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl simple ./tiamo reach tests/als.xml -cora -order DFS -incl simple
Input automaton parsed, computing LU bounds Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds Took 0 seconds to compute LU bounds
we have explored 285000 states, 10152 in the waiting listt
discrete states: 1736 discrete states: 41
states seen: 376461 states seen: 51
states explored: 285190 states explored: 20
max size of storage: 317837 max size of storage: 51
incl tests: 1208691736 incl tests: 20
pos. incl tests: 1215266 pos. incl tests: 0
Result of verification is Reachable! Result of verification is Reachable!
Path is Path is
Aicraft Landing System model, reachability, BFS, abstract inclusion test Aicraft Landing System model, reachability, DFS, abstract inclusion test
./tiamo reach tests/als.xml -cora -order BFS -incl sri ./tiamo reach tests/als.xml -cora -order DFS -incl sri
Input automaton parsed, computing LU bounds Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds Took 0 seconds to compute LU bounds
we have explored 5000 states, 3000 in the waiting list
discrete states: 1736 discrete states: 41
states seen: 15918 states seen: 51
states explored: 9722 states explored: 20
max size of storage: 10087 max size of storage: 51
incl tests: 433035 incl tests: 20
pos. incl tests: 47330 pos. incl tests: 0
Result of verification is Reachable! Result of verification is Reachable!
Path is 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