Commit 1261c427 authored by Tobias Meggendorfer's avatar Tobias Meggendorfer

Changes

parent dd4face8
# Each line is composed as follows
# (MODELFILE; PROPERTYFILE; PROPERTYNAME; CONSTS; EXPECTEDRESULT)
(crowds.prism; crowds.props; positive; TotalRuns=5,CrowdSize=20; 0.08606905443651044)
(crowds.prism; crowds.props; positive; TotalRuns=6,CrowdSize=20; 0.12047637088459826)
(egl.prism; egl.props; unfairA; N=10,L=2; ; )
(egl.prism; egl.props; unfairA; N=10,L=8; ; )
(haddad-monmege.pm; haddad-monmege.prctl; target; N=100,p=0.7; 0.7)
(consensus.4.prism; consensus.props; disagree; K=4; 0.15607306398806395)
(consensus.6.prism; consensus.props; disagree; K=2; ; )
(csma.3-4.prism; csma.props; all_before_max; ; 0.9324469288458124)
(csma.3-4.prism; csma.props; some_before; ; 0.9895225981437074)
(csma.4-2.prism; csma.props; all_before_max; ; 0.7764601493129573)
(firewire.false.prism; firewire.false.props; deadline; delay=36,deadline=800; ; )
(pacman.nm; pacman.props; crash; MAXSTEPS=60; 0.5511074970678996)
(pacman.nm; pacman.props; crash; MAXSTEPS=100; 0.5511176224662503)
(pnueli-zuck.5.prism; pnueli-zuck.props; live; ; )
(pnueli-zuck.10.prism; pnueli-zuck.props; live; ; )
(rabin.10.prism; rabin.10.props; live; ,)
(resource-gathering.pm; resource-gathering.prctl; prgoldgem; B=1300,GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100; )
# (wlan.4.prism; wlan.props; sent; COL=0; true)
# (wlan.5.prism; wlan.props; sent; COL=0; true)
# (wlan.6.prism; wlan.props; sent; COL=0; true)
(zeroconf.prism; zeroconf.props; correct_max; N=1000,K=8,reset=false; 4.801363180722697e-8)
(zeroconf.prism; zeroconf.props; correct_min; N=1000,K=8,reset=false; 5.040105212929839e-9)
#!/usr/bin/env bash
if [[ -z "$1" ]]; then
echo "Need to pass a configuration file";
else
grep -v '^#' $1 | while IFS= read -r line; do
echo ${line} | tr -d '( )' | awk -F';' '{printf "-m data/models/%s -p data/properties/%s -n %s",
$1, $2, $3; if (length($4) != 0) printf " --const " $4; if (length($5) != 0) printf " --expected " $5; print "" }'
done
fi
[
{
"benchmark-id": "pnueli-zuck.5.live",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m pnueli-zuck.5.prism -p pnueli-zuck.props --property live "
]
},
{
"benchmark-id": "pnueli-zuck.10.live",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m pnueli-zuck.10.prism -p pnueli-zuck.props --property live "
]
},
{
"benchmark-id": "rabin.10.live",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m rabin.10.prism -p rabin.10.props --property live "
]
},
{
"benchmark-id": "zeroconf.1000-8-false.correct_max",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m zeroconf.prism -p zeroconf.props --property correct_max --const N=1000,K=8,reset=false"
]
},
{
"benchmark-id": "zeroconf.1000-8-false.correct_min",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m zeroconf.prism -p zeroconf.props --property correct_min --const N=1000,K=8,reset=false"
]
},
{
"benchmark-id": "embedded.8-12.actuators",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m embedded.prism -p embedded.props --property actuators --const N=1000,K=8,reset=false"
]
},
{
"benchmark-id": "embedded.8-12.actuators",
"invocation-id": "specific",
"invocation-note": "DIFFERENCE is a slightly more greedy sampling heuristic which performs way better on this model",
"commands": [
"./pet/bin/pet reachability --heuristic DIFFERENCE --precision 0.001 --relative-error --only-result -m embedded.prism -p embedded.props --property actuators --const N=1000,K=8,reset=false"
]
},
{
"benchmark-id": "csma.3-4.all_before_max",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m csma.3-4.prism -p csma.props --property all_before_max",
]
}
]
\ No newline at end of file
[
{
"benchmark-id": "polling.18-16.s1_before_s2",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m polling.18.prism -p polling.props --property s1_before_s2 --const T=16"
]
},
{
"benchmark-id": "wlan.4-0.sent",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m wlan.4.prism -p wlan.props --property sent --const COL=0"
]
},
{
"benchmark-id": "wlan.5-0.sent",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m wlan.5.prism -p wlan.props --property sent --const COL=0"
]
},
{
"benchmark-id": "wlan.6-0.sent",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m wlan.6.prism -p wlan.props --property sent --const COL=0"
]
},
{
"benchmark-id": "haddad-monmege.100-0.7.target",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m haddad-monmege.pm -p haddad-monmege.prctl --property target --const N=100,p=0.7"
]
},
{
"benchmark-id": "csma.3-4.some_before",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m csma.3-4.prism -p csma.props --property some_before "
]
},
{
"benchmark-id": "pacman.60.crash",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m pacman.nm -p pacman.props --property crash --const MAXSTEPS=60"
]
},
{
"benchmark-id": "pacman.100.crash",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --relative-error --only-result -m pacman.nm -p pacman.props --property crash --const MAXSTEPS=100"
]
},
{
"benchmark-id": "crowds.5-20.positive",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m crowds.prism -p crowds.props --property positive --const TotalRuns=5,CrowdSize=20"
]
},
{
"benchmark-id": "crowds.6-20.positive",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m crowds.prism -p crowds.props --property positive --const TotalRuns=6,CrowdSize=20"
]
},
{
"benchmark-id": "egl.10-2.unfairA",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m egl.prism -p egl.props --property unfairA --const N=10,L=2"
]
},
{
"benchmark-id": "egl.10-8.unfairA",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m egl.prism -p egl.props --property unfairA --const N=10,L=8"
]
},
{
"benchmark-id": "nand.40-4.reliable",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m nand.prism -p nand.props --property reliable --const N=40,K=4"
]
},
{
"benchmark-id": "nand.60-4.reliable",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --precision 0.001 --only-result -m nand.prism -p nand.props --property reliable --const N=60,K=4"
]
},
{
"benchmark-id": "consensus.4-4.disagree",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --only-result -m consensus.4.prism -p consensus.props --property disagree -const K=4"
]
},
{
"benchmark-id": "consensus.4-4.steps_min",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --only-result -m consensus.4.prism -p consensus.props --property steps_min -const K=4"
]
},
{
"benchmark-id": "consensus.6-2.disagree",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --only-result -m consensus.6.prism -p consensus.props --property disagree -const K=2"
]
},
{
"benchmark-id": "consensus.6-2.steps_min",
"invocation-id": "default",
"invocation-note": "Default settings.",
"commands": [
"./pet/bin/pet reachability --only-result -m consensus.6.prism -p consensus.props --property steps_min -const K=2"
]
}
]
\ No newline at end of file
// nand multiplex system
// gxn/dxp 20/03/03
// U (correctly) performs a random permutation of the outputs of the previous stage
dtmc
const int N; // number of inputs in each bundle
const int K; // number of restorative stages
const int M = 2*K+1; // total number of multiplexing units
// parameters taken from the following paper
// A system architecture solution for unreliable nanoelectric devices
// J. Han & P. Jonker
// IEEEE trans. on nanotechnology vol 1(4) 2002
const double perr = 0.02; // probability nand works correctly
const double prob1 = 0.9; // probability initial inputs are stimulated
// model whole system as a single module by resuing variables
// to decrease the state space
module multiplex
u : [1..M]; // number of stages
c : [0..N]; // counter (number of copies of the nand done)
s : [0..4]; // local state
// 0 - initial state
// 1 - set x inputs
// 2 - set y inputs
// 3 - set outputs
// 4 - done
z : [0..N]; // number of new outputs equal to 1
zx : [0..N]; // number of old outputs equal to 1
zy : [0..N]; // need second copy for y
// initially 9 since initially probability of stimulated state is 0.9
x : [0..1]; // value of first input
y : [0..1]; // value of second input
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
// choose x permute selection (have zx stimulated inputs)
// note only need y to be random
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
// choose x randomly from selection (have zy stimulated inputs)
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
// use nand gate
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
[] s=4 -> true;
endmodule
// rewards: final value of gate
rewards
[] s=0 & (c=N) & (u=M) : z/N;
endrewards
// Probability to reach the target state
"target": P=? [F "target"];
"Target": P=? [F "target"];
// Expected number of steps to reach the target or the sink state
"exp_steps": T=? [F "done"];
// "exp_steps": T=? [F "done"];
// Probability that less than 10 percent of outputs are erroneous
// RESULT (N=20,K=1): 0.28641904
// RESULT (N=20,K=2): 0.41286262
// RESULT (N=20,K=3): 0.46854396
// RESULT (N=20,K=4): 0.49415805
// RESULT (N=40,K=1): 0.28648730
// RESULT (N=40,K=2): 0.48380547
// RESULT (N=40,K=3): 0.57770691
// RESULT (N=40,K=4): 0.61868222
// RESULT (N=60,K=1): 0.26946099
// RESULT (N=60,K=2): 0.51753355
"reliable": P=? [ F s=4 & z/N<0.1 ];
# Each line is composed as follows
# (MODELFILE; PROPERTYFILE; PROPERTYNAME; CONSTS; EXPECTEDRESULT)
(crowds.prism; crowds.props; positive; TotalRuns=3,CrowdSize=5; 0.05296253509523565)
(crowds.prism; crowds.props; positive; TotalRuns=6,CrowdSize=5; 0.19916173482259542)
(crowds.prism; crowds.props; positive; TotalRuns=5,CrowdSize=10; 0.10478678887151971)
(egl.prism; egl.props; unfairA; N=5,L=2; ; 0.515625)
(egl.prism; egl.props; unfairA; N=5,L=6; ; 0.515625)
(egl.prism; egl.props; unfairA; N=5,L=8; ; 0.515625)
(haddad-monmege.pm; haddad-monmege.props; target; N=20,p=0.7; 0.7)
(haddad-monmege.pm; haddad-monmege.props; target; N=100,p=0.7; 0.7)
(haddad-monmege.pm; haddad-monmege.props; target; N=300,p=0.7; 0.7)
(consensus.2.prism; consensus.props; disagree; K=2; 0.10833333333333334)
(consensus.4.prism; consensus.props; disagree; K=2; 0.29443185428958624)
(consensus.4.prism; consensus.props; disagree; K=4; 0.15607306398806395)
(csma.2-2.prism; csma.props; all_before_max; ; 0.875)
(csma.2-6.prism; csma.props; all_before_max; ; 0.9999995231628418)
(csma.3-2.prism; csma.props; some_before; ; 0.5859375)
(pacman.nm; pacman.props; crash; MAXSTEPS=5; 0.5511)
(pacman.nm; pacman.props; crash; MAXSTEPS=60; 0.5511074970678996)
(resource-gathering.pm; resource-gathering.props; prgoldgem; B=200,GOLD_TO_COLLECT=15,GEM_TO_COLLECT=15; 0.8080456033115208)
(resource-gathering.pm; resource-gathering.props; prgoldgem; B=400,GOLD_TO_COLLECT=30,GEM_TO_COLLECT=30; 0.8647565951595304)
(wlan.0.prism; wlan.props; sent; COL=0; true)
(wlan.2.prism; wlan.props; sent; COL=0; true)
(wlan.3.prism; wlan.props; sent; COL=0; true)
(zeroconf.prism; zeroconf.props; correct_max; N=20,K=2,reset=true; 0.000020103281776956928)
(zeroconf.prism; zeroconf.props; correct_max; N=20,K=2,reset=false; 0.000020119576888287857)
(zeroconf.prism; zeroconf.props; correct_max; N=1000,K=2,reset=false; 0.001060796942774321)
\ No newline at end of file
......@@ -19,7 +19,7 @@ public class StateValuesBoundedReachability implements StateValuesBounded {
@Override
public Bounds bounds(int state, int remainingSteps) {
checkArgument(0 <= remainingSteps, "Negative remaining steps %s", remainingSteps);
assert 0 <= remainingSteps;
Bounds reachabilityBounds = reachability.get(state);
if (reachabilityBounds != null) {
......
......@@ -144,6 +144,8 @@ public final class Util {
int index = 0;
IntIterator iterator = support.iterator();
while (iterator.hasNext()) {
assert index < size;
int successor = iterator.nextInt();
if (ignoreSuccessors.test(successor)) {
continue;
......
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