Build the benchmark in bench/gspn-ssp/ using makefiles
This commit is contained in:
Alexandre Duret-Lutz
parent
b83349d416
commit
56d1dbc610
20 changed files with 8643 additions and 146 deletions
69
bench/gspn-ssp/tools/bench-create
Executable file
69
bench/gspn-ssp/tools/bench-create
Executable file
|
|
@ -0,0 +1,69 @@
|
|||
#!/bin/sh
|
||||
|
||||
if test ! -d models; then
|
||||
echo "Error: this script should be run from the parent of the models/ directory." 2>&1
|
||||
exit 1
|
||||
fi
|
||||
|
||||
out=bench.mk
|
||||
rm -f $out
|
||||
exec >$out
|
||||
|
||||
echo "# This file is automatically generated by bench-create, do not edit."
|
||||
echo
|
||||
|
||||
F=50
|
||||
|
||||
allres=
|
||||
|
||||
cd models
|
||||
for i in *; do
|
||||
|
||||
Ffile=models/$i/formulae
|
||||
echo "############################## $i ##############################"
|
||||
echo
|
||||
echo "models/$i/formulae: models/$i/stamp"
|
||||
echo " mkdir -p results"
|
||||
echo " \$(top_builddir)/src/ltltest/randltl -F $F -u -s 0 -f 10 -r 7 \`cat models/$i/$i.ap\` > \$@"
|
||||
echo
|
||||
|
||||
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
|
||||
|
||||
case $check in
|
||||
*L) check="${check%L} -L";;
|
||||
*n) check="${check%n} -n";;
|
||||
esac
|
||||
check="${check## } $ltl2tgba"
|
||||
|
||||
resall=`echo results/$i.$check | tr -d ' ' `
|
||||
all=
|
||||
for fi in `seq 1 $F`; do
|
||||
res=`echo $resall-$fi.log | tr -d ' ' `
|
||||
echo "$res: $Ffile"
|
||||
echo " \$(run_bench) $Ffile $fi '-$check' $i > \$@.tmp"
|
||||
echo " mv \$@.tmp \$@"
|
||||
all="$all $res"
|
||||
done
|
||||
|
||||
echo
|
||||
echo "$resall.all: $all"
|
||||
echo " \$(collate) $all > \$@.tmp"
|
||||
echo " mv \$@.tmp \$@"
|
||||
echo
|
||||
|
||||
allres="$allres $resall.all"
|
||||
done
|
||||
done
|
||||
cd ..
|
||||
done
|
||||
|
||||
echo "RESULTS =$allres"
|
||||
|
||||
cd ..
|
||||
chmod -w $out
|
||||
13
bench/gspn-ssp/tools/collate
Executable file
13
bench/gspn-ssp/tools/collate
Executable file
|
|
@ -0,0 +1,13 @@
|
|||
#!/bin/sh
|
||||
|
||||
for f in "$@"; do
|
||||
sed -n '/^$/n;
|
||||
/^Command exited with non-zero status/n;
|
||||
2,$s/[^0-9.]//g;
|
||||
s/^[.]//;
|
||||
1x;
|
||||
2,$H;
|
||||
$x;
|
||||
$s/\n/,/g;
|
||||
$p' "$f"
|
||||
done
|
||||
10
bench/gspn-ssp/tools/modelgen-create
Executable file
10
bench/gspn-ssp/tools/modelgen-create
Executable file
|
|
@ -0,0 +1,10 @@
|
|||
#!/bin/sh
|
||||
|
||||
if test ! -d template; then
|
||||
echo "Error: this script should be run from the parent of the template/ directory." 2>&1
|
||||
exit 1
|
||||
fi
|
||||
|
||||
rm -f modelgen.mk
|
||||
templates/gen > modelgen.mk
|
||||
chmod -w modelgen.mk
|
||||
32
bench/gspn-ssp/tools/runbench
Executable file
32
bench/gspn-ssp/tools/runbench
Executable file
|
|
@ -0,0 +1,32 @@
|
|||
#!/bin/sh
|
||||
|
||||
formula=`sed -n "$2{p;q}" $1`
|
||||
check=$3
|
||||
model=$4
|
||||
|
||||
. ./defs
|
||||
|
||||
cp -r models/$model tmp-$$
|
||||
cd tmp-$$
|
||||
case $model in
|
||||
*.rg)
|
||||
if [ ! -f $model.snow ]; then
|
||||
$TIME $LTLGSPNSRG $check $model "$formula" `cat $model.ap` 2>&1
|
||||
else
|
||||
PROPS=`echo $formula | sed 's/P[0-9]/&,\n/g' | sed 's/.*P/P/' |
|
||||
grep P | sort -u | tr -d '\n' | sed 's/,$//'`
|
||||
$SNOW -m $model.cami -p $model.snow -f "$PROPS"
|
||||
$TRANS2PL model
|
||||
mv model.nettmp model.net
|
||||
$TIME $LTLGSPNSRG $check $model "$formula" \
|
||||
`echo $PROPS | tr ',' ' '` 2>&1
|
||||
fi;;
|
||||
*)
|
||||
$TIME $LTLGSPNSSP $check $model "$formula" "$model.con" `cat $model.ap` 2>&1 ;;
|
||||
esac
|
||||
test -f $model.mark || touch $model.mark
|
||||
test -f $model.event || touch $model.event
|
||||
du -b *.mark *.event | cut -f 1
|
||||
|
||||
cd ..
|
||||
rm -rf tmp-$$
|
||||
238
bench/gspn-ssp/tools/sum
Executable file
238
bench/gspn-ssp/tools/sum
Executable file
|
|
@ -0,0 +1,238 @@
|
|||
#!/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",
|
||||
"inclusion count",
|
||||
"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",
|
||||
],
|
||||
);
|
||||
|
||||
$C{e45} = $C{e5};
|
||||
$C{e54} = $C{e5};
|
||||
$C{e5L} = $C{e5};
|
||||
$C{e5n} = $C{e5};
|
||||
$C{e45n} = $C{e5};
|
||||
|
||||
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.]+)\.(e.*)-f\.all$/;
|
||||
my $name = $1;
|
||||
my $meth = $2;
|
||||
|
||||
$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 = "$model.$meth";
|
||||
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,\.all,,;
|
||||
$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";
|
||||
}
|
||||
}
|
||||
89
bench/gspn-ssp/tools/trans2prop.pl
Executable file
89
bench/gspn-ssp/tools/trans2prop.pl
Executable file
|
|
@ -0,0 +1,89 @@
|
|||
#!/usr/bin/perl -w
|
||||
|
||||
use strict 'vars';
|
||||
|
||||
die "Please specify model name as first argument to script.\n"
|
||||
unless 1 != $#ARGV;
|
||||
|
||||
my $modelname = $ARGV[0];
|
||||
#print "Will work on model \"$modelname\"\n";
|
||||
my $netf = "$modelname.net";
|
||||
my $deff = "$modelname.def";
|
||||
my $propf = "$modelname.tobs";
|
||||
my $tmpf = "$modelname.nettmp";
|
||||
open (NET, "< $netf") or die "cannot open $netf\n";
|
||||
open (DEF, "< $deff") or die "cannot open $deff\n";
|
||||
open (PROP, "> $propf") or die "cannot open $propf\n";
|
||||
open (OUTNET,"> $tmpf") or die "cannot open $tmpf\n";
|
||||
|
||||
|
||||
my %defs = ();
|
||||
{
|
||||
local $/;
|
||||
my $contents = <DEF>;
|
||||
close DEF;
|
||||
while ($contents =~ /\((F\d+)\s[^\(]*\(\@f\n(.*)\n\)\)/gom)
|
||||
{
|
||||
$defs{$1} = $2;
|
||||
}
|
||||
}
|
||||
|
||||
my $line = <NET>;
|
||||
print OUTNET $line;
|
||||
$line = <NET>;
|
||||
print OUTNET $line;
|
||||
|
||||
$line = <NET>;
|
||||
my @split = split (/\s+/, $line);
|
||||
|
||||
my $nump = $split[2];
|
||||
my $numt = $split[4];
|
||||
|
||||
#print "$nump places, $numt transitions\n";
|
||||
|
||||
my $places ;
|
||||
for (my $i = 0; $i < $nump; $i++)
|
||||
{
|
||||
$places .= <NET>;
|
||||
}
|
||||
my %trans = ();
|
||||
my $transline = <NET>;
|
||||
for (my $i = 0; $i < $numt; $i++)
|
||||
{
|
||||
my $tname = (split (/ /,$transline))[0];
|
||||
$trans{$tname} .= $transline;
|
||||
$trans{$tname} .= $line while (defined ($line = <NET>) && $line =~ /^\s/);
|
||||
# print "analyzed transition $tname:\n$trans{$tname}\n";
|
||||
$transline = $line;
|
||||
}
|
||||
|
||||
my $numpt = grep /^PROP\_/, keys %trans;
|
||||
$split[4] -= $numpt ;
|
||||
|
||||
print OUTNET (join (" ",@split));
|
||||
print OUTNET "\n";
|
||||
print OUTNET $places;
|
||||
print PROP "$numpt\n";
|
||||
my $props = '';
|
||||
foreach my $key (keys %trans)
|
||||
{
|
||||
if ($key =~ /^PROP_/)
|
||||
{
|
||||
$props .= $trans{$key};
|
||||
}
|
||||
else
|
||||
{
|
||||
print OUTNET $trans{$key}
|
||||
}
|
||||
}
|
||||
|
||||
$props =~ s/^PROP_//gm;
|
||||
while (my ($key, $val) = each %defs)
|
||||
{
|
||||
$props =~ s/$key\s*$/$val/gm;
|
||||
}
|
||||
|
||||
close OUTNET;
|
||||
print PROP $props;
|
||||
close PROP;
|
||||
close NET;
|
||||
Loading…
Add table
Add a link
Reference in a new issue