Commit 1bc7cdf2 authored by Maximilien Colange's avatar Maximilien Colange

Merge branch 'tests'

parents a0eda0df 0850e631
...@@ -51,4 +51,10 @@ TESTS = \ ...@@ -51,4 +51,10 @@ TESTS = \
tests/test_9.data \ tests/test_9.data \
tests/test_10.data \ tests/test_10.data \
tests/test_11.data \ tests/test_11.data \
tests/test_12.data tests/test_12.data \
tests/test_13.data \
tests/test_14.data \
tests/test_15.data \
tests/test_16.data \
tests/test_17.data \
tests/test_18.data
...@@ -9,13 +9,34 @@ chomp $title; ...@@ -9,13 +9,34 @@ chomp $title;
my $call = <IN>; my $call = <IN>;
chomp $call; chomp $call;
my $nominal ; my $nominal;
my %expected;
while (my $line = <IN>) { while (my $line = <IN>) {
chomp $line; chomp $line;
if ($line =~ s/Result of verification is //) { if ($line =~ s/Result of verification is //) {
$nominal = $line; $nominal = $line;
last; }
# gather stats
if ($line =~ s/^discrete states://) {
my @splitline = split(' ',$line);
$expected{"ds"} = $splitline[0];
}
if ($line =~ s/^states seen://) {
my @splitline = split(' ',$line);
$expected{"ss"} = $splitline[0];
}
if ($line =~ s/^states explored://) {
my @splitline = split(' ',$line);
$expected{"se"} = $splitline[0];
}
if ($line =~ s/^incl tests://) {
my @splitline = split(' ',$line);
$expected{"incl"} = $splitline[0];
}
if ($line =~ s/^pos\. incl tests://) {
my @splitline = split(' ',$line);
$expected{"pincl"} = $splitline[0];
} }
} }
...@@ -40,23 +61,38 @@ while (my $line = shift(@results)) { ...@@ -40,23 +61,38 @@ while (my $line = shift(@results)) {
# report some stats to teamcity # report some stats to teamcity
if ($line =~ s/^discrete states://) { if ($line =~ s/^discrete states://) {
my @splitline = split(' ',$line); my @splitline = split(' ',$line);
print "##teamcity[buildStatisticValue key='discrete states' value='$splitline[0]']\n"; my $exp = $expected{"ds"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of discrete states $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
} }
if ($line =~ s/^states seen://) { if ($line =~ s/^states seen://) {
my @splitline = split(' ',$line); my @splitline = split(' ',$line);
print "##teamcity[buildStatisticValue key='states seen' value='$splitline[0]']\n"; my $exp = $expected{"ss"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of states seen $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
} }
if ($line =~ s/^states explored://) { if ($line =~ s/^states explored://) {
my @splitline = split(' ',$line); my @splitline = split(' ',$line);
print "##teamcity[buildStatisticValue key='states explored' value='$splitline[0]']\n"; my $exp = $expected{"se"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of states explored $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
} }
if ($line =~ s/^incl tests://) { if ($line =~ s/^incl tests://) {
my @splitline = split(' ',$line); my @splitline = split(' ',$line);
print "##teamcity[buildStatisticValue key='inclusion tests' value='$splitline[0]']\n"; my $exp = $expected{"incl"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of inclusion tests $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
} }
if ($line =~ s/^pos\. incl tests://) { if ($line =~ s/^pos\. incl tests://) {
my @splitline = split(' ',$line); my @splitline = split(' ',$line);
print "##teamcity[buildStatisticValue key='successful inclusion tests' value='$splitline[0]']\n"; my $exp = $expected{"pincl"};
if ($splitline[0] != $exp) {
print "##teamcity[message text='number of successful inclusiontests $splitline[0] differs from nominal $exp' status='WARNING']\n";
}
} }
} }
......
#! /bin/sh #! /bin/bash
# teamcity-test-driver - basic testsuite driver script that reports tests results in # teamcity-test-driver - basic testsuite driver script that reports tests results in
# TeamCity format # TeamCity format
# this file derives from the basic autotools test-driver (cf copyright below) # this file derives from the basic autotools test-driver (cf copyright below)
...@@ -106,6 +106,7 @@ trap "st=141; $do_exit" 13 ...@@ -106,6 +106,7 @@ trap "st=141; $do_exit" 13
trap "st=143; $do_exit" 15 trap "st=143; $do_exit" 15
# Test script is run here. # Test script is run here.
set -o pipefail
"$@" 2>&1 | tee $log_file "$@" 2>&1 | tee $log_file
estatus=$? estatus=$?
......
...@@ -3,16 +3,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, abstract inclusio ...@@ -3,16 +3,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, abstract inclusio
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
new optimal value 90 replaces 1073741823, found after seeing 826 states new optimal value 90 replaces 1073741823, found after seeing 1202 states
corresponding path has length 14 corresponding path has length 20
cleaning: shrink from 1837 states to 410 states stored cleaning: shrink from 2866 states to 554 states stored
still 1161 states waiting for treatment still 1931 states waiting for treatment
discrete states: 272 discrete states: 434
states seen: 2081 states seen: 3290
states explored: 826 states explored: 1202
max size of storage: 1846 max size of storage: 2881
incl tests: 41882 incl tests: 60046
pos. incl tests: 1732 pos. incl tests: 3089
Result of verification is 90 Result of verification is 90
Path is Path is
...@@ -2,17 +2,17 @@ Vehicule Routing model, optimal reachability, BBFS cost, abstract inclusion test ...@@ -2,17 +2,17 @@ Vehicule Routing model, optimal reachability, BBFS cost, abstract inclusion test
./tiamo optimal tests/vrptw.xml -cora -order BBFS -best cost -incl exp -p ./tiamo optimal tests/vrptw.xml -cora -order BBFS -best cost -incl exp -p
Input automaton parsed, computing LU bounds Input automaton parsed, computing LU bounds
Took 175 seconds to compute LU bounds Took 0 seconds to compute LU bounds
new optimal value 18372 replaces 1073741823, found after seeing 135092 states new optimal value 18372 replaces 1073741823, found after seeing 136922 states
corresponding path has length 27 corresponding path has length 27
cleaning: shrink from 144191 states to 135017 states stored cleaning: shrink from 146051 states to 136847 states stored
still 9570 states waiting for treatment still 9600 states waiting for treatment
discrete states: 29853 discrete states: 29853
states seen: 151502 states seen: 153382
states explored: 135092 states explored: 136922
max size of storage: 144419 max size of storage: 146279
incl tests: 1486881 incl tests: 1549095
pos. incl tests: 24875 pos. incl tests: 24617
Result of verification is 18372 Result of verification is 18372
Path is Path is
Energy Task Scheduling model, simple reachability, BFS, simple inclusion test
./tiamo reach tests/ets.xml -cora -order BFS -incl simple
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
discrete states: 55
states seen: 249
states explored: 209
max size of storage: 226
incl tests: 1791
pos. incl tests: 179
Result of verification is Reachable!
Path is
Energy Task Scheduling model, simple reachability, BFS, abstract inclusion test
./tiamo reach tests/ets.xml -cora -order BFS -incl sri
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
discrete states: 55
states seen: 68
states explored: 64
max size of storage: 65
incl tests: 74
pos. incl tests: 51
Result of verification is Reachable!
Path is
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
Energy Task Scheduling model, optimal reachability, BFS, abstract inclusion test
./tiamo optimal tests/ets.xml -cora -order BFS -incl exp
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 1340 replaces 1073741823, found after seeing 79 states
corresponding path has length 13
new optimal value 1320 replaces 1340, found after seeing 79 states
corresponding path has length 13
discrete states: 55
states seen: 94
states explored: 80
max size of storage: 80
incl tests: 141
pos. incl tests: 58
Result of verification is 1320
Path is
Energy Task Scheduling model, optimal reachability, SBFS, simple inclusion test
./tiamo optimal tests/ets.xml -cora -order SBFS -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 1320 replaces 1073741823, found after seeing 497 states
corresponding path has length 13
discrete states: 55
states seen: 654
states explored: 654
max size of storage: 582
incl tests: 18144
pos. incl tests: 462
Result of verification is 1320
Path is
Energy Task Scheduling model, optimal reachability, SBFS, abstract inclusion test
./tiamo optimal tests/ets.xml -cora -order SBFS -incl exp
Input automaton parsed, computing LU bounds
Took 0 seconds to compute LU bounds
new optimal value 1320 replaces 1073741823, found after seeing 81 states
corresponding path has length 13
discrete states: 55
states seen: 107
states explored: 85
max size of storage: 83
incl tests: 174
pos. incl tests: 66
Result of verification is 1320
Path is
...@@ -2,11 +2,12 @@ Fischer model, reachability, BFS, abstract inclusion test ...@@ -2,11 +2,12 @@ Fischer model, reachability, BFS, abstract inclusion test
./tiamo reach tests/fischer.xml -incl sri ./tiamo reach tests/fischer.xml -incl sri
Input automaton parsed, computing LU bounds Input automaton parsed, computing LU bounds
we have explored 200000 states, 530 in the waiting listtt Took 0 seconds to compute LU bounds
we have explored 220000 states, 3903 in the waiting listt
discrete states: 7737 discrete states: 7737
states seen: 200530 states seen: 223903
states explored: 200530 states explored: 223903
max size of storage: 200530 max size of storage: 223903
incl tests: 85510147 incl tests: 109940539
pos. incl tests: 483595 pos. incl tests: 483595
Result of verification is Not reachable... Result of verification is Not reachable...
...@@ -2,11 +2,12 @@ Fischer model, reachability, DFS, abstract inclusion test ...@@ -2,11 +2,12 @@ Fischer model, reachability, DFS, abstract inclusion test
./tiamo reach tests/fischer.xml -order DFS -incl sri ./tiamo reach tests/fischer.xml -order DFS -incl sri
Input automaton parsed, computing LU bounds Input automaton parsed, computing LU bounds
we have explored 255000 states, 14 in the waiting listtt Took 0 seconds to compute LU bounds
we have explored 275000 states, 14 in the waiting listtt
discrete states: 7737 discrete states: 7737
states seen: 258725 states seen: 279454
states explored: 258688 states explored: 279454
max size of storage: 200530 max size of storage: 223903
incl tests: 112802714 incl tests: 138320181
pos. incl tests: 661849 pos. incl tests: 659242
Result of verification is Not reachable... Result of verification is Not reachable...
...@@ -4,16 +4,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, simple inclusion ...@@ -4,16 +4,16 @@ Aicraft Landing System model, optimal reachability, BBFS cost, simple inclusion
[WARNING] If your automaton is not acyclic or bounded, the chosen inclusion test does not guarantee termination. [WARNING] If your automaton is not acyclic or bounded, the chosen inclusion test does not guarantee termination.
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
new optimal value 90 replaces 1073741823, found after seeing 1186 states new optimal value 90 replaces 1073741823, found after seeing 2330 states
corresponding path has length 14 corresponding path has length 20
cleaning: shrink from 2879 states to 436 states stored cleaning: shrink from 5703 states to 910 states stored
still 1841 states waiting for treatment still 3630 states waiting for treatment
discrete states: 272 discrete states: 434
states seen: 3085 states seen: 6057
states explored: 1186 states explored: 2330
max size of storage: 2887 max size of storage: 5712
incl tests: 138544 incl tests: 374896
pos. incl tests: 1540 pos. incl tests: 3854
Result of verification is 90 Result of verification is 90
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