Open xhajnal opened 5 years ago
PRISM ===== Version: 4.4 Date: Sun Mar 17 21:11:20 CET 2019 Hostname: Freya Memory limits: cudd=1g, java(heap)=27.6g Command line: prism /home/matej/Git/mpm/models/multiparam_semisynchronous_20.pm /home/matej/Git/mpm/properties/prop_20.pctl -javamaxmem 31g -param 'p=0:1,q1=0:1,q2=0:1,q3=0:1,q4=0:1,q5=0:1,q6=0:1,q7=0:1,q8=0:1,q9=0:1,q10=0:1,q11=0:1,q12=0:1,q13=0:1,q14=0:1,q15=0:1,q16=0:1,q17=0:1,q18=0:1,q19=0:1' -property 23 Parsing model file "/home/matej/Git/mpm/models/multiparam_semisynchronous_20.pm"... Parsing properties file "/home/matej/Git/mpm/properties/prop_20.pctl"... 23 properties: (1) P=? [ F (a0=0)&(a1=0)&(a2=0)&(a3=0)&(a4=0)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (2) P=? [ F (a0=1)&(a1=0)&(a2=0)&(a3=0)&(a4=0)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (3) P=? [ F (a0=1)&(a1=1)&(a2=0)&(a3=0)&(a4=0)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (4) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=0)&(a4=0)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (5) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=0)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (6) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=0)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (7) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=0)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (8) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=0)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (9) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=0)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (10) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=0)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (11) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=0)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (12) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=0)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (13) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=0)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (14) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=0)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (15) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=0)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (16) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=0)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (17) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=1)&(a16=0)&(a17=0)&(a18=0)&(a19=0) ] (18) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=1)&(a16=1)&(a17=0)&(a18=0)&(a19=0) ] (19) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=1)&(a16=1)&(a17=1)&(a18=0)&(a19=0) ] (20) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=1)&(a16=1)&(a17=1)&(a18=1)&(a19=0) ] (21) P=? [ F (a0=1)&(a1=1)&(a2=1)&(a3=1)&(a4=1)&(a5=1)&(a6=1)&(a7=1)&(a8=1)&(a9=1)&(a10=1)&(a11=1)&(a12=1)&(a13=1)&(a14=1)&(a15=1)&(a16=1)&(a17=1)&(a18=1)&(a19=1) ] (22) R{"mean"}=? [ F b=1 ] (23) R{"mean_squared"}=? [ F b=1 ] Type: DTMC Modules: multi_param_agents_20 Variables: a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 b --------------------------------------------------------------------- Parametric model checking: R{"mean_squared"}=? [ F b=1 ] Building model (parametric engine)... Computing reachable states... Reachable states exploration and model construction done in 0.186 secs. States: 234 (1 initial) Transitions: 444 Time for model construction: 0.186 seconds. Building reward structure... /home/matej/prism-4.4-linux64/bin/prism: line 86: 19796 Killed "$PRISM_JAVA" $PRISM_JAVA_ARG1 $PRISM_JAVA_ARG2 $PRISM_JAVA_DEBUG $PRISM_JAVAMAXMEM $PRISM_JAVASTACKSIZE -Djava.awt.headless=$PRISM_HEADLESS -Djava.library.path="$JAVA_LIBRARY_PATH" -classpath "$PRISM_CLASSPATH" $PRISM_MAINCLASS "$@"
xhajnal
commented
5 years ago xhajnal
commented
5 years ago