xhajnal / DiPS

Multiple properties Probabilistic systems Model checker
BSD 3-Clause "New" or "Revised" License
4 stars 1 forks source link

PRISM memory Error not detected (multiparam_asynchronous_20) #26

Closed xhajnal closed 5 years ago

xhajnal commented 5 years ago
PRISM
=====

Version: 4.4
Date: Mon Mar 11 19:30:45 CET 2019
Hostname: Freya
Memory limits: cudd=1g, java(heap)=27.6g
Command line: prism /home/matej/Git/mpm/models/multiparam_asynchronous_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_asynchronous_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:     multiparam_bees_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.152 secs.

States:      443 (1 initial)
Transitions: 843

Time for model construction: 0.153 seconds.
Building reward structure...
OpenJDK 64-Bit Server VM warning: INFO: os::commit_memory(0x00007fe665980000, 1786773504, 0) failed; error='Cannot allocate memory' (errno=12)
#
# There is insufficient memory for the Java Runtime Environment to continue.
# Native memory allocation (mmap) failed to map 1786773504 bytes for committing reserved memory.
# An error report file with more information is saved as:
# /home/matej/prism-4.4-linux64/bin/hs_err_pid22980.log
xhajnal commented 5 years ago

just a memory alloc failure, it may help to alloc only available amount of memory at the time