Merge branch 'tests'

Makefile.am

@@ -45,4 +45,10 @@ TESTS = \
 	tests/test_3.data \
 	tests/test_4.data \
 	tests/test_5.data \
-	tests/test_6.data
+	tests/test_6.data \
+	tests/test_7.data \
+	tests/test_8.data \
+	tests/test_9.data \
+	tests/test_10.data \
+	tests/test_11.data \
+	tests/test_12.data

run_test.pl

@@ -37,6 +37,27 @@ while (my $line = shift(@results)) {
   if ($line =~ s/Result of verification is //) {
     $tested = $line;
   }
+  # report some stats to teamcity
+  if ($line =~ s/^discrete states://) {
+    my @splitline = split(' ',$line);
+    print "##teamcity[buildStatisticValue key='discrete states' value='$splitline[0]']\n";
+  }
+  if ($line =~ s/^states seen://) {
+    my @splitline = split(' ',$line);
+    print "##teamcity[buildStatisticValue key='states seen' value='$splitline[0]']\n";
+  }
+  if ($line =~ s/^states explored://) {
+    my @splitline = split(' ',$line);
+    print "##teamcity[buildStatisticValue key='states explored' value='$splitline[0]']\n";
+  }
+  if ($line =~ s/^incl tests://) {
+    my @splitline = split(' ',$line);
+    print "##teamcity[buildStatisticValue key='inclusion tests' value='$splitline[0]']\n";
+  }
+  if ($line =~ s/^pos\. incl tests://) {
+    my @splitline = split(' ',$line);
+    print "##teamcity[buildStatisticValue key='successful inclusion tests' value='$splitline[0]']\n";
+  }
 }
 
 # retrieve the exit value of the test
@@ -47,18 +68,22 @@ if ($? == 0) {
   $failure = 1;
 }
 
-my $tc_output = join("|n|r", @outputs);
+my $tc_output = join("|n", @outputs);
+# escape characters for TeamCity
+$tc_output =~ s/\[/\|\[/g;
+$tc_output =~ s/\]/\|\]/g;
+$tc_output =~ s/'/\|'/g;
 my $reg_output = join("\n", @outputs);
-if ( $nominal ne $tested ) {
-  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 ) {
+if ( $failure ) {
   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";
+} elsif ( $nominal ne $tested ) {
+  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";
 } else {
 #   print "##teamcity[buildStatisticValue key='testDuration' value='@tested[2]']\n";
 #   print "##teamcity[buildStatisticValue key='testMemory' value='@tested[3]']\n";

src/reachability.ml

@@ -563,9 +563,9 @@ struct
 
   let to_string ta (res,path) =
     if (res = Dbm.PDbm.Dbm.infty) then
-      "not reachable..."
+      "Not reachable..."
     else
-      Printf.sprintf "%d with path\n%s" res (Walker.path_to_string ta path)
+      Printf.sprintf "%d\nPath is\n%s" res (Walker.path_to_string ta path)
 
 end
 

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 -v mylog=$log_file '{if (/teamcity/) print ; else print > mylog; }'`
+"$@" 2>&1 | tee $log_file
 estatus=$?
 
 # estatus should always be 0
@@ -122,9 +122,9 @@ if test $estatus -ne 0; then
 else
   # the result of the test is determined by teamcity report messages
   # detect them to properly set the status of the test in 'make check' report
-  if echo "$TC_OUTPUT" | grep "##teamcity\[testIgnored"; then
+  if grep "##teamcity\[testIgnored" $log_file; then
     tweaked_estatus=77
-  elif echo "$TC_OUTPUT" | grep "##teamcity\[testFailed"; then
+  elif grep "##teamcity\[testFailed" $log_file; then
     tweaked_estatus=1
   else
     tweaked_estatus=0
@@ -147,8 +147,6 @@ esac
 echo "$res $test_name (exit status: $estatus)" >>$log_file
 
 # Report outcome to console.
-# do not forget to report Teamcity service messages
-echo "$TC_OUTPUT"
 echo "${col}${res}${std}: $test_name"
 
 # Register the test result, and other relevant metadata.

tests/test_10.data

+Aicraft Landing System model, optimal reachability, BBFS cost, abstract inclusion test, with pruning
+./tiamo optimal tests/als.xml -cora -order BBFS -best cost -incl exp -p
+
+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
+
+discrete states:	272
+states seen:		2081
+states explored:	826
+max size of storage:	1846
+incl tests:		41882
+pos. incl tests:	1732
+Result of verification is 90
+Path is

tests/test_11.data

+Vehicule Routing model, optimal reachability, BBFS cost, simple inclusion test, with pruning
+./tiamo optimal tests/vrptw.xml -cora -order BBFS -best cost -incl simple -p
+
+[WARNING] If your automaton is not acyclic or bounded, the chosen inclusion test does not guarantee termination.
+Input automaton parsed, computing LU bounds
+Took 184 seconds to compute LU bounds
+new optimal value 18372 replaces 1073741823, found after seeing 354815 states
+corresponding path has length 27
+cleaning: shrink from 379778 states to 354716 states stored
+still 25209 states waiting for treatment
+
+discrete states:	29853
+states seen:		393235
+states explored:	354815
+max size of storage:	380138
+incl tests:		15995559
+pos. incl tests:	150920
+Result of verification is 18372
+Path is

tests/test_12.data

+Vehicule Routing model, optimal reachability, BBFS cost, abstract inclusion test, with pruning
+./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
+corresponding path has length 27
+cleaning: shrink from 144191 states to 135017 states stored
+still 9570 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
+Result of verification is 18372
+Path is

tests/test_7.data

+Aicraft Landing System model, reachability, BFS, simple inclusion test
+./tiamo reach tests/als.xml -cora -order BFS -incl simple
+
+Input automaton parsed, computing LU bounds
+Took 0 seconds to compute LU bounds
+we have explored 285000 states, 10152 in the waiting listt
+discrete states:	1736
+states seen:		376461
+states explored:	285190
+max size of storage:	317837
+incl tests:		1208691736
+pos. incl tests:	1215266
+Result of verification is Reachable!
+Path is

tests/test_8.data

+Aicraft Landing System model, reachability, BFS, abstract inclusion test
+./tiamo reach tests/als.xml -cora -order BFS -incl sri
+
+Input automaton parsed, computing LU bounds
+Took 0 seconds to compute LU bounds
+we have explored 5000 states, 3000 in the waiting list
+discrete states:	1736
+states seen:		15918
+states explored:	9722
+max size of storage:	10087
+incl tests:		433035
+pos. incl tests:	47330
+Result of verification is Reachable!
+Path is

tests/test_9.data

+Aicraft Landing System model, optimal reachability, BBFS cost, simple inclusion test, with pruning
+./tiamo optimal tests/als.xml -cora -order BBFS -best cost -incl simple -p
+
+[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
+
+discrete states:	272
+states seen:		3085
+states explored:	1186
+max size of storage:	2887
+incl tests:		138544
+pos. incl tests:	1540
+Result of verification is 90
+Path is