Commit 35bf9b53 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

bench/gspn-ssp/: New directory.

parent d3b5e5bd
2008-08-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* bench/gspn-ssp/Makefile.am, bench/gspn-ssp/trans2prop.pl: New files.
* bench/gspn-ssp/config: Rename as bench/gspn-ssp/defs.in.
* bench/Makefile.am (SUBDIRS): Add gspn-ssp.
* configure.ac: Output bench/gspn-ssp/Makefile and bench/gspn-ssp/defs.
* bench/gspn-ssp/bench: Include defs.
2008-08-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* bench/gspn-ssp/: New directory. Contains some of the benches
used in baarir.06.tr03, baarir.07.acsd, and baarir.07.msr.
2008-08-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/gspn/ltlgspn.cc: New option: -e54.
......
## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
## Copyright (C) 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
##
......@@ -19,4 +19,4 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
SUBDIRS = emptchk ltl2tgba
SUBDIRS = emptchk gspn-ssp ltl2tgba
## Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
## dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
## et Marie Curie.
##
## This file is part of Spot, a model checking library.
##
## Spot is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published by
## the Free Software Foundation; either version 2 of the License, or
## (at your option) any later version.
##
## Spot is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
## License for more details.
##
## You should have received a copy of the GNU General Public License
## along with Spot; see the file COPYING. If not, write to the Free
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
EXTRA_DIST = \
bench \
benchaux \
gen \
sum \
sumall \
templates/bagrodia/bagrodia.con \
templates/bagrodia/bagrodia.def \
templates/bagrodia/bagrodia.gd \
templates/bagrodia/bagrodia.net \
templates/bagrodia/bagrodia.prop \
templates/bagrodia/gen \
templates/common \
templates/gen \
templates/predef/gen \
templates/predef/WCSasym10.def \
templates/predef/WCSasym10.net \
templates/predef/WCSasym10.tobs \
templates/predef/WCSasym2.def \
templates/predef/WCSasym2.net \
templates/predef/WCSasym2.tobs \
templates/predef/WCSasym3.def \
templates/predef/WCSasym3.net \
templates/predef/WCSasym3.tobs \
templates/predef/WCSasym4.def \
templates/predef/WCSasym4.net \
templates/predef/WCSasym4.tobs \
templates/predef/WCSasym5.def \
templates/predef/WCSasym5.net \
templates/predef/WCSasym5.tobs \
templates/predef/WCSasym6.def \
templates/predef/WCSasym6.net \
templates/predef/WCSasym6.tobs \
templates/predef/WCSasym8.def \
templates/predef/WCSasym8.net \
templates/predef/WCSasym8.tobs \
templates/WCSsym/gen \
templates/WCSsym/WCSsym.con \
templates/WCSsym/WCSsym.def \
templates/WCSsym/WCSsym.gd \
templates/WCSsym/WCSsym.net \
templates/WCSsym/WCSsym.prop \
trans2prop.pl
#!/bin/sh
. ./defs
H=`pwd`
test -d results || mkdir results
cd models
[ $# -eq 0 ] && set -- *
for i; do
cd $i
for ltl2tgba in -f; do
case $i in
*.rg) checks=e2;;
*) checks='e4 e6 e5 e5L e5n e2 e45 e45n';;
esac
for check in $checks; do
res=$H/results/$i.RES-$check$ltl2tgba
test -f $res && continue
export res check i ltl2tgba
rm -f $res
$TIME "$H/benchaux" 2>$res-TOTAL
done
done
cd ..
done
#!/bin/sh -x
case $check in
*L) check="${check%L} -L";;
*n) check="${check%n} -n";;
esac
set -x
$RANDLTL -F 50 -u -s 0 -f 10 -r 7 `cat $i.ap` |
while read f; do
echo "Running with $f on $i with -$check $ltl2tgba"
(case $i in
*.rg)
if [ ! -f $i.snow ]; then
$TIME $LTLGSPNSRG -$check $ltl2tgba $i "$f" `cat $i.ap` 2>&1
else
PROPS=`echo $f | sed 's/P[0-9]/&,\n/g' | sed 's/.*P/P/' |
grep P | sort -u | tr -d '\n' | sed 's/,$//'`
$SNOW -m $i.cami -p $i.snow -f "$PROPS"
$TRANS2PL model
mv model.nettmp model.net
$TIME $LTLGSPNSRG -$check $ltl2tgba model "$f" \
`echo $PROPS | tr ',' ' '` 2>&1
fi;;
*)
$TIME $LTLGSPNSSP -$check $ltl2tgba $i "$f" "$i.con" `cat $i.ap` 2>&1 ;;
esac
test -f *.mark || touch "x.mark"
test -f *.event || touch "x.event"
du -b *.mark *.event | cut -f 1
) |
tee tmp
sed -n '/^$/n;
/^Command exited with non-zero status/n;
2,$s/[^0-9.]//g;
s/^[.]//;
1x;
2,$H;
$x;
$s/\n/,/g;
$p' < tmp >> $res
done
# -*- shell-script -*-
# Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
# Ensure we are running from the right directory.
test -f ./defs || {
echo "defs: not found in current directory" 1>&2
exit 1
}
srcdir='@srcdir@'
# Ensure $srcdir is set correctly.
test -f "$srcdir/defs.in" || {
echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
exit 1
}
RANDLTL='@top_builddir@/src/ltltest/randltl'
LTLGSPNSSP='@top_builddir@/iface/gspn/ltlgspn-ssp'
LTLGSPNSRG='@top_builddir@/iface/gspn/ltlgspn-srg'
SNOW=/home/adl/projs/src/gspn/snow
TRANS2PL='@srcdir@/trans2prop.pl'
TIME='/usr/bin/time -p'
export RANDLTL LTLGSPNSSP LTLGSPNSRG TIME SNOW TRANS2PL
#!/bin/sh
cd templates && ./gen
#!/usr/bin/env perl
use warnings;
use strict;
my %C = (
e2 => [
"formulae",
"unique states visited",
"SCC in search stack",
"max. depth",
"removed components",
"states",
"transitions",
"vmsize",
"real",
"user",
"sys",
".mark size",
".event size",
"mem total",
],
e4 => [
"formulae",
"unique states visited",
"SCC in search stack",
"contained map size",
"find_state count",
"max. depth",
"removed components",
"states",
"transitions",
"vmsize",
"real",
"user",
"sys",
".mark size",
".event size",
"mem total",
],
e45 => [
"formulae",
"unique states visited",
"SCC in search stack",
"contained map size",
"inclusion count heap",
"inclusion count stack",
"max. depth",
"removed components",
"states",
"transitions",
"vmsize",
"real",
"user",
"sys",
".mark size",
".event size",
"mem total",
],
e5 => [
"formulae",
"unique states visited",
"SCC in search stack",
"contained map size",
"inclusion count heap",
"inclusion count stack",
"max. depth",
"removed components",
"states",
"transitions",
"vmsize",
"real",
"user",
"sys",
".mark size",
".event size",
"mem total",
],
e6 => [
"formulae",
"unique states visited",
"SCC in search stack",
"contained map size",
"inclusion count heap",
"inclusion count stack",
"max. depth",
"removed components",
"states",
"transitions",
"vmsize",
"real",
"user",
"sys",
".mark size",
".event size",
"mem total",
],
);
my %filter = (states => 1, transitions => 1, user => 1);
my %order = (e2 => 2, e6 => 3, e5 => 4, e4 => 5);
my %H;
my %S;
my %P;
while (<>)
{
my @l = split (/,/);
push @l, ($l[-1] + $l[-2] + $l[-6] * 4096)/1024;
my $e = shift @l;
$e =~ s/non empty/non e./;
$ARGV =~ /([\w.]+).RES-(\w+)/;
my $name = $1;
my $meth = $2;
$meth =~ s/[nL]$//;
$P{$name}{$e}{$meth} = 1;
if (!exists $H{$meth}{$ARGV}{$e})
{
$H{$meth}{$ARGV}{$e} = [1, @l];
$S{$meth} = 1 + @l;
}
else
{
$H{$meth}{$ARGV}{$e}->[0]++;
for (my $i = 0; $i < @l; ++$i)
{
$H{$meth}{$ARGV}{$e}->[$i + 1] += $l[$i];
}
}
}
sub model_sort ($$)
{
my ($a, $b) = @_;
$a =~ s/\.rg//;
$a =~ s/.*(\d)$/$1$&/;
$b =~ s/\.rg//;
$b =~ s/.*(\d)$/$1$&/;
return $a cmp $b;
};
if (exists $ENV{FORTETABLE})
{
foreach my $e ("non e.", "empty")
{
foreach my $model (sort model_sort keys %P)
{
if (exists $P{$model}{$e})
{
foreach my $meth (sort { $order{$a} <=> $order{$b} }
keys %{$P{$model}{$e}})
{
my $n = "results/$model.RES-$meth-f";
next unless exists $H{$meth}{$n}{$e};
my @l = @{$H{$meth}{$n}{$e}};
print " "x17 . "% $model $meth $e\n";
my $st = $l[-5]/$l[0];
my $tr = $l[-4]/$l[0];
my $T = $l[-2]/$l[0];
my $res = $T >= 10 ? 1 : 2;
$res = 0 if $T >= 100;
printf "%17s& %.0f & %.0f & %.${res}f\n", "", $st, $tr, $T;
}
}
}
}
#if not exists $filter{$C{$meth}->[$i]};
exit 0;
}
foreach my $meth (sort keys %H)
{
printf "%21s", "";
foreach my $n (sort keys %{$H{$meth}})
{
$n =~ s,.*/,,;
$n =~ s,\.RES,,;
$n =~ s,-f,,;
printf "%18s", $n;
}
print "\n";
printf "%21s", "";
foreach my $n (sort keys %{$H{$meth}})
{
my $x = 2;
foreach my $k (keys %{$H{$meth}{$n}})
{
printf "%9s", $k;
$x--;
}
print " " x (9*$x);
}
print "\n";
for (my $i = 0; $i < $S{$meth}; ++$i)
{
printf "%-22s", $C{$meth}->[$i];
foreach my $n (sort keys %{$H{$meth}})
{
my $x = 2;
foreach my $k (keys %{$H{$meth}{$n}})
{
my @l = @{$H{$meth}{$n}{$k}};
if ($i)
{
printf "%8.2f ", $l[$i]/$l[0];
}
else
{
printf "%5dx ", $l[$i];
}
$x--
}
print " " x (9*$x);
}
print "\n";
}
}
#!/bin/sh
[ $# -eq 0 ] && set results/*.RES-*
for i; do
case $i in
*-TOTAL);;
*)
x="$x $i";
;;
esac
done
./sum $x
|256
%
|
(C1 c 13.416667 3.266667 (@c
{@PR@}
))
(C c 13.183333 3.116667 (@c
u C1
))
(M m 13.200000 3.566667 (@m
<S C1>
))
|0|
|
f 0 5 0 5 0 0 0
Req 0 3.700000 1.900000 3.900000 1.866667 0 3.900000 2.033333 C
Idle -10003 3.666667 4.083333 3.866667 4.050000 0 3.866667 4.216667 C
Wav 0 5.650000 1.916667 5.850000 1.883333 0 5.850000 2.050000 C
Att 0 7.583333 1.966667 7.783333 1.933333 0 7.783333 2.100000 C
Cs 0 10.450000 4.166667 10.650000 4.133333 0 10.650000 4.300000 C
T1 1.000000 0 0 1 0 3.650000 2.983333 3.483333 2.866667 3.816667 3.066667 0
1 2 0 0 0.000000 0.000000 <x>
1
1 1 0 0 0.000000 0.000000 <x>
0
T2 1.000000 0 0 1 1 4.683333 1.900000 4.516667 1.783333 4.850000 1.983333 0
1 1 0 0 0.000000 0.000000 <x>
1
1 3 0 0 0.000000 0.000000 <x>
2
1 4 1 0 0.000000 0.000000 <S>
5.983333 2.583333
1 5 1 0 0.000000 0.000000 <S>
5.900000 3.150000
T3 1.000000 0 0 1 1 6.583333 1.950000 6.416667 1.833333 6.750000 2.033333 0
1 3 0 0 0.000000 0.000000 <x>
1
1 4 0 0 0.000000 0.000000 <x>
0
T6 1.000000 0 0 1 1 10.400000 1.933333 10.233333 1.816667 10.566667 2.016667 0
1 4 0 0 0.000000 0.000000 <x>
1
1 5 0 0 0.000000 0.000000 <x>
2
1 5 1 0 0.000000 0.000000 <S>
10.033333 3.083333
1 3 2 0 0.000000 0.000000 <S>
10.316667 0.950000
5.650000 0.900000
T7 1.000000 0 0 1 1 7.133333 4.083333 6.966667 3.966667 7.300000 4.166667 0
1 5 0 0 0.000000 0.000000 <x>
1
1 2 0 0 0.000000 0.000000 <x>
0
P1: Att >= <pr1>;
P2: Cs >= 2<pr1>;
P3: Req >= <pr1>;
P4: Idle >= 2<pr1>;
P5: Att >= 2<pr2>;
P6: #(Att) >= 2;
P7: Wav >= <pr2>;
P8: Req >= <pr2>;
#!/bin/sh
for i in 3 4 5 6 8 ; do
sfx=$i
. ../common
PRS=`seq 1 $i | sed 's/^/pr/;s/$/,/' | tr -d '\n' | sed 's/,$//'`
sed "s/@PR@/$PRS/" "$name.def" > "$dst/$name$sfx.def"
sed "s/:.*//" < "$name.prop" | tr '\n' ' ' > "$dst/$name$sfx.ap"
done
|256
%
|
(x c 7.966667 1.233333 (@c
{@X@}
))
(X c 7.933333 1.033333 (@c
u x
))
(m c 8.950000 1.050000 (@c
{d,r,a}
))
(M c 8.816667 0.733333 (@c
u m
))
(Mar m 9.066667 1.450000 (@m
<S>
))
r_retard[m={d} and z=MAXC(x,z)];
r_ech3[m={d} and m1={r}];
r_ech2[m={d} and m1={r} and x=MAXC(x,z)];
succ[m={d,a}];
s_retard[m={d,a} and m1={r}];
rej_retard[m={r} and m1={a}];
r_succ[m={d}];
rejet[m={r}];
dem[m={d}];
|0|
|
f 0 9 0 16 1 0 0
Repos -10005 2.166667 2.766667 2.366667 2.733333 0 2.366667 2.900000 X
Appel 0 4.633333 2.833333 4.833333 2.800000 0 4.833333 2.966667 X
EnCours 0 6.866667 2.783333 7.066667 2.750000 0 7.066667 2.916667 X
Pot 0 3.383333 5.016667 3.583333 4.983333 0 3.583333 5.150000 X,X
Att 0 9.550000 4.283333 9.750000 4.250000 0 9.750000 4.416667 X,X
Jeton 0 4.633333 7.416667 4.833333 7.383333 0 4.833333 7.550000 X,X
Succ 0 6.300000 9.766671 6.500000 9.733333 0 6.500000 9.900000 X,X
Retarde 0 11.850000 3.533333 12.050000 3.500000 0 12.050000 3.666667 X,X
Message 0 11.200000 7.633333 11.400000 7.600000 0 11.400000 7.766667 M,X,X
G5 0.000000 0.000000 1
r_ech1 1.000000e+00 0 0 1 0 7.783333 9.233329 7.616667 9.116667 7.950000 9.316667 0
1 9 0 0 0.000000 0.000000 <m,z,x>
1
1 9 1 0 0.000000 0.000000 <m1,x,z>
9.850000 9.300000
1
1 4 0 0 0.000000 0.000000 <x,z>
r_ech2 1.000000e+00 0 0 3 0 7.750000 8.516667 7.583333 8.400000 7.916667 8.600000 0 7.916667 8.400000 [z<>y]
1 9 0 0 0.000000 0.000000 <m,z,x>
1 4 1 0 0.000000 0.000000 <x,z>
5.933333 7.183333
1 5 1 0 0.000000 0.000000 <x,y>
9.366667 6.466667
3
1 9 1 0 0.000000 0.000000 <m1,x,z>
8.350002 8.700000
1 4 1 0 0.000000 0.000000 <x,z>
6.450000 6.883333
1 5 1 0 0.000000 0.000000 <x,y>
9.250000 6.100000
0
r_ech3 1.000000e+00 0 0 3 0 7.700000 7.150000 7.533333 7.033333 7.866667 7.233333 0 7.866667 7.033333 [z<>y]
1 8 1 0 0.000000 0.000000 <x,w>
7.850000 3.016667