Commit b0c820f6 authored by Benoît Barbot's avatar Benoît Barbot

gen graph

parent 248dfa3b
Pipeline #962 failed with stages
in 4 minutes and 27 seconds
#set -e
nb_points=${2:-10000}
size_poly=${3:-10}
loopsize=${4:-10}
sage script_tocosmos_PTA.sage $1 $1.grml $size_poly -1 -unif
Cosmos $1.grml --loop "#$loopsize" --trace-place "x_1,x_2,x_3,t_a,t_b,t_c,t_a1,t_a2,t_b1,t_b2" --output-trace $1.dat 0.0 --max-run "$nb_points" --use-van-der-corput --set-Horizon "$loopsize" --batch 0 --width 0
#grep 'time_' $1.dat > preplot.dat
grep 't_a' $1.dat > preplota.dat
grep 't_b' $1.dat > preplotb.dat
grep 't_c' $1.dat > preplotc.dat
#linecombinator $1.dat preplot.dat
gnuplot -c gnplotscript.gp $1_VDC.png
Cosmos $1.grml --loop "#$loopsize" --trace-place "x_1,x_2,x_3,t_a,t_b,t_c,t_a1,t_a2,t_b1,t_b2" --output-trace $1.dat 0.0 --max-run "$nb_points" --batch 0 --width 0
#grep 'time_' $1.dat > preplot.dat
#grep 'time_0_0\|time_1_0\|time_2_0' $1.dat > preplota.dat
#grep 'time_0_1\|time_1_1\|time_2_1\|time_3_0' $1.dat > preplotb.dat
#grep 'time_0_2\|time_1_2\|time_2_2\|time_3_1' $1.dat > preplotc.dat
grep 't_a' $1.dat > preplota.dat
grep 't_b' $1.dat > preplotb.dat
grep 't_c' $1.dat > preplotc.dat
#linecombinator $1.dat preplot.dat
gnuplot -c gnplotscript.gp $1_Unif.png
Cosmos Iso_$1.grml --loop "#$loopsize" --trace-place "x_1,x_2,x_3,t_a,t_b,t_c,t_a1,t_a2,t_b1,t_b2" --output-trace Iso_$1.dat 0.0 --max-run "$nb_points" --batch 0 --width 0
grep 't_a' Iso_$1.dat > preplota.dat
grep 't_b' Iso_$1.dat > preplotb.dat
grep 't_c' Iso_$1.dat > preplotc.dat
#grep 'tt_' Iso_$1.dat > preplot.dat
#grep 'tt_0_0\|tt_1_0\|tt_2_0' Iso_$1.dat > preplota.dat
#grep 'tt_0_1\|tt_1_1\|tt_2_1\|tt_3_0' Iso_$1.dat > preplotb.dat
#grep 'tt_0_2\|tt_1_2\|tt_2_2\|tt_3_1' Iso_$1.dat > preplotc.dat
#linecombinator Iso_$1H.dat preplot.dat
gnuplot -c gnplotscript.gp $1_Iso.png
#set -e
nb_points=${2:-10000}
size_poly=${3:-10}
loopsize=${4:-10}
sage script_tocosmos_PTA.sage $1 $1.grml $size_poly -1 -unif
echo "$1_Unif.png";
Cosmos $1.grml taTacas2018.lha --tmp-status 2 --output-raw histdata.raw --max-run "$nb_points" --const "N=$loopsize" --tmp-status 2 --set-Horizon "$loopsize"
gnuplot -c histogram.gnu "$1_Unif.png"
Cosmos Iso_$1.grml taTacas2018.lha --tmp-status 2 --output-raw histdata.raw --max-run "$nb_points" --const "N=$loopsize" --tmp-status 2 --set-Horizon "$loopsize"
gnuplot -c histogram.gnu "$1_ISO.png"
Cosmos $1.grml taTacas2018.lha --tmp-status 2 --output-raw histdata.raw --max-run "$nb_points" --const "N=$loopsize" --tmp-status 2 --set-Horizon "$loopsize" --use-van-der-corput
gnuplot -c histogram.gnu "$1_VDC.png"
set terminal png size 1400,1400
set terminal svg size 400,400
set style line 1 lt 1 lw 4 lc rgb '#A0A0A0'
......@@ -10,7 +10,7 @@ set style line 5 lt 3 lw 7 lc rgb '#FFA02F'
set output ARG1
set pointsize 0.1
set pointsize 0.1
set tic font ",22"
......@@ -19,4 +19,4 @@ set ytic 1
plot 'preplota.dat' using 2:3 notitle with points pt 7 lc rgb '#FFA02F',\
'preplotb.dat' using 2:3 notitle with points pt 7 lc rgb '#829600',\
'preplotc.dat' using 2:3 notitle with points pt 7 lc rgb '#800080'
\ No newline at end of file
'preplotc.dat' using 2:3 notitle with points pt 7 lc rgb '#800080'
# set width of single bins in histogram
set boxwidth 0.9*binwidth
# set fill style of bins
set style fill solid 0.5
# define macro for plotting the histogram
hist = 'u (binwidth*(floor(($1-binstart)/binwidth)+0.5)+binstart):(1.0) smooth freq w boxes'
hist2= 'u (binwidth*(floor(($2-binstart)/binwidth)+0.5)+binstart):(1.0) smooth freq w boxes'
set terminal png
set output ARG1
set xrange [-0.5 :*]
binwidth = 1
binstart = -0.5
load 'hist.fct'
plot 'histdata.raw' i 0 @hist ls 1,\
'' i 0 @hist2 ls 2
......@@ -5,7 +5,7 @@ import os
import re
from exportGrML import *
## Set Parameters
## Set Parameters
#prismpath="prism";
#prismpath="/Users/barbot/Documents/discrepancy/prism-ptasmc/prism/bin/prism";
prismpath="~/Documents/prism/prism-ptasmc/prism/bin/prism ";
......@@ -29,20 +29,20 @@ Dline=-1;
if len(sys.argv)>4:
Dline = int(sys.argv[4])
isIsotropic=False;
isIsotropic=False;
if len(sys.argv)>5:
if sys.argv[5] == "-isotropic" :
isIsotropic = True;
all_miniedge = True;
all_miniedge = True;
objregexp= re.compile('')
if len(sys.argv)>5:
objregexp=re.compile(sys.argv[5])
################################################################################
################################################################################
## Launch Prism
## Launch Prism
print(str(sys.argv[1]) + ' -> ' + sagepath + '.sage' );
retval=os.system(prismpath + ' ' + str(sys.argv[1]) + ' -exportsplitreach ' + sagepath + '.sage');
print(sagepath + '.sage -> ' + outpath );
......@@ -103,14 +103,14 @@ def clockO(list,i,l): #In the ith state the lth clock is either equal to 0 eithe
if yy[i][l-1]==0:
return 0;
return list[yy[i][l-1]-1];
def WeightsPdfCdf(f): #Compute one iteration of operator Op with all weights/pdf/cdf computed for this iteration.
psiDeltaf=[]; #psiDeltaf[i][j][k] weight of Delta
Cdf=[]; #Integ[i][j][k][e] primitive of f(r(x+t)) wrt t;
Pdf=[];
for state in statelist:
i=state['id'];
psiDeltaf.append([]);
psiDeltaf.append([]);
Cdf.append([]);
Pdf.append([]);
j=-1;
......@@ -123,7 +123,7 @@ def WeightsPdfCdf(f): #Compute one iteration of operator Op with all weights/pdf
pol1=f[edge['target']];
listcoef=[(edge['reset'][l])*(clockO(x,i,l+1)+t) for l in range(cardclocks)];#the reset depend on the mini-edge
listcoef.append(0);
if pol1 != 0:
if pol1 != 0:
pdf=pol1(listcoef);
else:
pdf=R(0);
......@@ -187,7 +187,7 @@ def printGRML_place(statelist):
#The place before choosing time associated to transition i,j if more than 1 action
if(len(state['transition'])>1):
s+= printGRML_OnePlace('12%d' %(trans['id']),'s_%d_%d_2' %(i,j), 0 );
#The place after choosing time, before choosing mini-edge if more than 1 miniedge
if(len(trans['miniedge'])>1 or all_miniedge):
s+= printGRML_OnePlace('30%d' %(trans['id']),'s_%d_%d_3' %(i,j), 0 );
......@@ -226,7 +226,7 @@ def printGRML_distribution(alldistr,idtransinv,statelist,data_path,cardclocks,fi
normid,cdfid,pdfid);
#fichier_data.write("//fin distr\n")
return((s,tabidDistrHorizon));
def get_reset(cardclocks,edge):
t='<attribute name=\"update\">\n ';
for c in range(cardclocks):
......@@ -263,18 +263,18 @@ def printGRML_transition(statelist,allones,isIsotropic,Dline):
#poids de la transition i j
nbpoly2 = max(nbpoly2,poly_to_data(allones[k]['psiDeltaf'][i][j],fichier_data,cardclocks,' //weight'));
t+=' <attribute name=\"unParsed\"> customDistr.evalPoly(%d - %s' %(nbpoly2,horizon);
t+= ', { %s ,0.0}) </attribute>\n' %passingClockParameters; #C est quoi ca -> c'est pour passer les valeur d'horloge
#Pour cosmos les horloge sont juste des variable il faut mapper les variable du polynomes aux horloges
#if only 1 action do not generate transition
#if only 1 action do not generate transition
if( len(state['transition']) >1):
s+=printGRML_OneInstaTransition('13%d' %(trans['id']),
'action_%d_%d_%s' %(i,j,trans['action']),
'1',
t,
'');
#choose time
t="" #time
r="" #reset
......@@ -287,9 +287,9 @@ def printGRML_transition(statelist,allones,isIsotropic,Dline):
#if only 1 miniedge compute reset
r="";
if(len(trans['miniedge'])==1 and not all_miniedge):
if(len(trans['miniedge'])==1 and not all_miniedge):
r=get_reset(cardclocks,trans['miniedge'][0]);
s+=printGRML_OneTransition('16%d' %(trans['id']),
'time_%d_%d' %(i,j),
t,
......@@ -322,7 +322,7 @@ def printGRML_arc(statelist):
s+=printGRML_OneArc('17', '12%d' %(trans['id']), '16%d' %(trans['id']));
else:
s+=printGRML_OneArc('14', "11%d" %(state['id']), '16%d' %(trans['id']));
s+=printGRML_OneArc('23', '16%d' %(trans['id']), '20%d' %action);#C est quoi? -> ca active une transition qui porte le meme label que l'action
s+=printGRML_OneArc('23', '16%d' %(trans['id']), '20%d' %action);#C est quoi? -> ca active une transition qui porte le meme label que l'action
s+=printGRML_OneArc('31', '16%d' %(trans['id']), '240');#C est quoi? -> ca compte le nombre d'action
if(len(trans['miniedge'])==1 and not all_miniedge):
edge = trans['miniedge'][0];
......@@ -334,7 +334,7 @@ def printGRML_arc(statelist):
for edge in trans['miniedge']:#NEW
s+=printGRML_OneArc('24', '30%d' %(trans['id']), '25%d' %(edge['id']));
s+=printGRML_OneArc('26', '25%d' %(edge['id']), '11%d' %(edge['target']));
if ( finstate[edge['target']]) :#Ca sert a quoi? c'est pour ecrire des formules (F s) ou s est un etat
if ( finstate[edge['target']]) :#Ca sert a quoi? c'est pour ecrire des formules (F s) ou s est un etat
s+=printGRML_OneArc('19', '16%d' %(trans['id']), '19');
return(s);
......@@ -342,7 +342,7 @@ def action_to_signal(a):
if a == 'a' :
return 1
else :
return -1
return 1
def toCOSMOS(allones,isIsotropic,Dline):
tab = '';
......
const int N=6;
VariablesList = {t, DISC n, DISC c, DISC c0, DISC c1,DISC c2,DISC c3, DISC ct} ;
LocationsList = {l0,l1, l2, lf1, lf2};
p=PROB(lf1);
av=AVG(Last(c));
av2=AVG(Last(ct));
%pdf = PDF(Last(r),0.05,0,1);
%cdf = CDF(Last(r),0.05,0,1);
InitialLocations = {l0};
FinalLocations = {lf1, lf2};
Locations={
(l0, TRUE , (t:1 ));
(l1, TRUE , (t:1 ));
(l2, TRUE , (t:1 ));
(lf1, TRUE , (t:1 ));
(lf2, TRUE , (t:1 ));
};
Edges={
((l0,l1),ALL\{t_a}, # , {c=0});
((l1,l1),ALL\{t_a}, # , #);
((l1,l1),{t_a}, n<=3, {n=n+1,c=2*c + floor(t),c0= floor(t), c1=c0, c2=c1,c3=c2, t=0});
((l1,l1),{t_a}, c0+c1+c2+c3 >=1 & c0+c1+c2+c3 <=2 & n>=4 & n<=N-1, {n=n+1,c=2*c + floor(t),c0= floor(t), c1=c0, c2=c1,c3=c2, t=0});
((l1,lf1),{t_a}, c0+c1+c2+c3 >=1 & c0+c1+c2+c3 <=2 & n=N ,{ct=-1 });
((l1,l2),{t_a}, c0+c1+c2+c3 <=1 & n>=4 & n<=N-1, {n=n+1,c=2*c + floor(t),c0= floor(t), c1=c0, c2=c1,c3=c2, t=0});
((l1,l2),{t_a}, c0+c1+c2+c3 >=2 & n>=4 & n<=N-1, {n=n+1,c=2*c + floor(t),c0= floor(t), c1=c0, c2=c1,c3=c2, t=0});
((l2,l2),ALL\{t_a}, # , #);
((l2,l2),{t_a}, n<=N-1, {n=n+1,c=2*c + floor(t),c0= floor(t), c1=c0, c2=c1,c3=c2, t=0});
((l2,lf2),{t_a}, n=N , {ct=c,c=-1});
((l1,lf2),{t_a}, c0+c1+c2+c3 <=1 & n=N ,{ct=c,c=-1});
((l1,lf2),{t_a}, c0+c1+c2+c3 >=2 & n=N ,{ct=c,c=-1});
};
pta
module controller
s : [0..1] init 0;
x : clock;
invariant
(x<2)
endinvariant
[a] (s=0) -> (s'=1);
[b] (s=1) -> (x'=0) & (s'=0);
[c] (s=0) -> (x'=0) & (s'=0);
endmodule
pta
module controller
s : [0..6] init 0;
x: clock;
x1 : clock;
x2 : clock;
x3 : clock;
x4 : clock;
invariant
(x<2) & (x1<6) & (x2<6) & (x3<6) & (x4<6)
endinvariant
[a] (s=0) -> (s'=1) & (x'=0) & (x1'=0) ;
[a] (s=1) -> (s'=2) & (x'=0) & (x2'=0) ;
[a] (s=2) -> (s'=3) & (x'=0) & (x3'=0) ;
[a] (s=3) & (x4>1) -> (s'=4) & (x'=0) & (x4'=0) ;
[a] (s=4) & (x1>1) -> (s'=5) & (x'=0) & (x1'=0) ;
[a] (s=5) & (x2>1) -> (s'=6) & (x'=0) & (x2'=0) ;
[a] (s=6) & (x3>1) -> (s'=3) & (x'=0) & (x3'=0) ;
endmodule
......@@ -4,7 +4,7 @@ NbLocations = 4 ;
VariablesList = {x, y,r,OK} ;
LocationsList = {l0, l1, l2, lp};
Overflow= 4*PROB;
Pi= 4*PROB;
%av=AVG(Mean(P2));
%pdf = PDF(Last(r),0.05,0,1);
%cdf = CDF(Last(r),0.05,0,1);
......
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