Commit c9813d1f authored by Maximilien Colange's avatar Maximilien Colange

Add 2 new tests.

parent ff61551f
......@@ -42,4 +42,6 @@ TESTS = \
tests/test_1.data \
tests/test_2.data \
tests/test_3.data \
tests/test_4.data
tests/test_4.data \
tests/test_5.data \
tests/test_6.data
<?xml version="1.0" encoding="UTF-8"?>
<nta>
<declaration>int id = 0;</declaration>
<template>
<name x="32" y="-16">P</name>
<parameter x="144" y="-16">const int pid</parameter>
<declaration>clock x;
const int k = 2;</declaration>
<location id="id2" x="216" y="176">
<name x="216" y="192">c</name>
</location>
<location id="id1" x="216" y="48">
<name x="216" y="16">b</name>
<label kind="invariant" x="240" y="32">x&lt;=k</label>
</location>
<location id="id0" x="64" y="48">
<name x="64" y="16">a</name>
</location>
<location id="id3" x="64" y="176">
<name x="56" y="192">cs</name>
</location>
<init ref="id0" />
<transition>
<source ref="id0" />
<target ref="id1" />
<label kind="guard" x="88" y="24">id== 0</label>
<label kind="assignment" x="160" y="24">x:= 0</label>
</transition>
<transition>
<source ref="id1" />
<target ref="id2" />
<label kind="guard" x="168" y="72">x&lt;=k</label>
<label kind="assignment" x="168" y="104">x:= 0,
id:= pid</label>
</transition>
<transition>
<source ref="id2" />
<target ref="id1" />
<label kind="guard" x="264" y="144">id== 0</label>
<label kind="assignment" x="264" y="64">x:= 0</label>
<nail x="251" y="146" />
<nail x="251" y="82" />
</transition>
<transition>
<source ref="id2" />
<target ref="id3" />
<label kind="guard" x="104" y="176">x&gt;k and id==pid</label>
</transition>
<transition>
<source ref="id3" />
<target ref="id0" />
<label kind="assignment" x="16" y="80">id:= 0</label>
</transition>
</template>
<system>P1 := P( 1 );
P2 := P( 2 );
P3 := P( 3 );
P4 := P( 4 );
P5 := P( 5 );
P6 := P( 6 );
P7 := P( 7 );
P8 := P( 8 );
P9 := P( 9 );
P10 := P( 10 );
P11 := P( 11 );
P12 := P( 12 );
system P1, P2, P3, P4, P5, P6, P7;</system>
<queries>
<query>
<formula>E&lt;&gt; (P2.cs and (P1.cs))
</formula>
<comment>
</comment>
</query>
</queries>
</nta>
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
discrete states: 7737
states seen: 200530
states explored: 200530
max size of storage: 200530
incl tests: 85510147
pos. incl tests: 483595
Result of verification is Not reachable...
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
discrete states: 7737
states seen: 258725
states explored: 258688
max size of storage: 200530
incl tests: 112802714
pos. incl tests: 661849
Result of verification is Not reachable...
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