Merge branch 'tests'

Makefile.am

@@ -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

run_test.pl

@@ -29,14 +29,13 @@ print "##teamcity[testStarted name='$title']\n";
 my $tested;
 
 my @outputs = ();
-my @results = `$call`;
+my @results = `$call 2>&1;`;
 
 while (my $line = shift(@results)) {
-  push (@outputs,$line);
   chomp $line;
+  push (@outputs,$line);
   if ($line =~ s/Result of verification is //) {
     $tested = $line;
-    last;
   }
 }
 
@@ -48,13 +47,15 @@ if ($? == 0) {
   $failure = 1;
 }
 
+my $tc_output = join("|n|r", @outputs);
+my $reg_output = join("\n", @outputs);
 if ( $nominal ne $tested ) {
-  print "@outputs\n";
-  print "\n##teamcity[testFailed name='$title' message='regression detected' details='' expected='$nominal' actual='$tested'] \n";
+  print "$reg_output\n";
+  print "\n##teamcity[testFailed name='$title' message='regression detected' details='$tc_output' expected='$nominal' actual='$tested'] \n";
   print "Expected :  $nominal  Obtained :  $tested \n";
 } elsif ( $failure ) {
-  print "@outputs\n";
-  print "\n##teamcity[testFailed name='$title' message='test did not exit properly' details='' expected='$nominal' actual='$tested'] \n";
+  print "$reg_output\n";
+  print "\n##teamcity[testFailed name='$title' message='test did not exit properly' details='$tc_output' expected='$nominal' actual='$tested'] \n";
   print "Expected :  $nominal  Obtained :  $tested \n"; 
   my $exitval = $? >> 8;
   print "test exited with value $exitval\n";

teamcity-test-driver

@@ -106,7 +106,7 @@ trap "st=141; $do_exit" 13
 trap "st=143; $do_exit" 15
 
 # Test script is run here.
-TC_OUTPUT=`"$@" 2>&1 | awk '{if (/teamcity/) print ; else print > "$log_file"; }'`
+TC_OUTPUT=`"$@" 2>&1 | awk -v mylog=$log_file '{if (/teamcity/) print ; else print > mylog; }'`
 estatus=$?
 
 # estatus should always be 0

tests/fischer.xml

+<?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>
+

tests/test_5.data

+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...

tests/test_6.data

+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...