search

xhajnal / DiPS

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

try parameter synthesis of polynomials using Storm #28

Closed xhajnal closed 5 years ago

xhajnal commented 5 years ago

storm-pars --prism some_model.pm --prop "P=? [F (A = 1)]"

xhajnal commented 5 years ago 
cd Git/mpm/

docker run --mount type=bind,source="$(pwd)",target=/mpm -w /opt/storm/build/bin --rm -it --name storm movesrwth/storm:travis

./storm --version

########################################################
            ORDINARY PARAMETER SYNTHESIS
########################################################
./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "P=? [F (a0=0)&(a1=0)]"
./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "R{\"mean\"}=? [ F b=1]"

(time ./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "R{\"mean\"}=? [ F b=1]") >> /mpm/storm_results/asynchronous_2_moments.txt 2>&1
(time ./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "R{\"mean_squared\"}=? [ F b=1]") >> /mpm/storm_results/asynchronous_2_moments.txt 2>&1

########################################################
Whole workflow
(time (./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "R{\"mean\"}=? [ F b=1]" 
       ./storm-pars --prism /mpm/models/asynchronous_2.pm --prop "R{\"mean_squared\"}=? [ F b=1]")) >> /mpm/storm_results/asynchronous_2_moments2.txt 2>&1

########################################################
ONE STEP FURTHER 

allpopulations=(2 3 5 10 20 40 50)
for t in ${allpopulations[@]}; do
    (time (./storm-pars --prism /mpm/models/asynchronous_$t.pm --prop "R{\"mean\"}=? [ F b=1]" 
           ./storm-pars --prism /mpm/models/asynchronous_$t.pm --prop "R{\"mean_squared\"}=? [ F b=1]")) >> /mpm/storm_results/asynchronous_$t\_moments.txt 2>&1
done

########################################################
ONE MORE STEP FURTHER 
SAVE THIS AS RUNALL.TXT
`

    #!/bin/bash
    allpopulations=(2 3 5 10 20 40 50)
    allmodels=('synchronous' 'semisynchronous' 'asynchronous')
    for m in ${allmodels[@]}; do
        for t in ${allpopulations[@]}; do
        (time (./storm-pars --prism /mpm/models/$m\_$t.pm --prop "R{\"mean\"}=? [ F b=1]" 
        ./storm-pars --prism /mpm/models/$m\_$t.pm --prop "R{\"mean_squared\"}=? [ F b=1]")) >> /mpm/storm_results/$m\_$t\_moments.txt 2>&1
        done
    done

bash /mpm/storm_results/runall.txt
xhajnal commented 5 years ago

Not fully automatized for the BSCC properties yet, but tried

xhajnal commented 5 years ago

solved in ba10b47a84ce530e9473efcb04ebfa7848082205