...
 
Commits (4)
......@@ -120,7 +120,7 @@ Rabin.10.live:
variables:
<<: *reach_variables
model: "data/models/rabin.10.prism"
property_file: "data/properties/rabin.10.props"
property_file: "data/models/rabin.10.props"
property: "live"
expected: "1.0"
<<: *reach_test_template
......@@ -129,7 +129,7 @@ Pnueli-Zuck.10.live:
variables:
<<: *reach_variables
model: "data/models/pnueli-zuck.10.prism"
property_file: "data/properties/pnueli-zuck.props"
property_file: "data/models/pnueli-zuck.props"
property: "live"
expected: "1.0"
<<: *reach_test_template
......@@ -139,7 +139,7 @@ Wlan.3.sent:
<<: *reach_variables
model: "data/models/wlan.2.prism"
const: "COL=0"
property_file: "data/properties/wlan.props"
property_file: "data/models/wlan.props"
property: "sent"
expected: "true"
heuristics: WEIGHTED GRAPH_WEIGHTED
......@@ -150,7 +150,7 @@ Zeroconf.1000-8-0.correct_max:
<<: *reach_variables
model: "data/models/zeroconf.prism"
const: "N=1000,K=8,reset=false"
property_file: "data/properties/zeroconf.props"
property_file: "data/models/zeroconf.props"
property: "correct_max"
expected: "4.80141363507243e-8"
<<: *reach_test_template
......@@ -160,7 +160,7 @@ Zeroconf.1000-8-0.correct_min:
<<: *reach_variables
model: "data/models/zeroconf.prism"
const: "N=1000,K=8,reset=false"
property_file: "data/properties/zeroconf.props"
property_file: "data/models/zeroconf.props"
property: "correct_min"
expected: "5.040105212929839e-9"
<<: *reach_test_template
......@@ -169,7 +169,7 @@ Csma.3-2.some_before:
variables:
<<: *reach_variables
model: "data/models/csma.3-2.prism"
property_file: "data/properties/csma.props"
property_file: "data/models/csma.props"
property: "some_before"
expected: "0.5859375"
<<: *reach_test_template
......@@ -178,7 +178,7 @@ Csma.3-2.all_before_min:
variables:
<<: *reach_variables
model: "data/models/csma.3-2.prism"
property_file: "data/properties/csma.props"
property_file: "data/models/csma.props"
property: "all_before_min"
expected: "0.43496662487687193"
<<: *reach_test_template
......@@ -187,7 +187,7 @@ Csma.3-2.all_before_max:
variables:
<<: *reach_variables
model: "data/models/csma.3-2.prism"
property_file: "data/properties/csma.props"
property_file: "data/models/csma.props"
property: "all_before_max"
expected: "0.8596150364756961"
<<: *reach_test_template
......@@ -197,7 +197,7 @@ Embedded.8-12.actuators:
<<: *reach_variables
model: "data/models/embedded.prism"
const: "MAX_COUNT=8,T=12"
property_file: "data/properties/embedded.props"
property_file: "data/models/embedded.props"
property: "actuators"
expected: "0.1053036557931282"
heuristics: DIFFERENCE
......@@ -208,7 +208,7 @@ Polling.8-16.actuators:
<<: *reach_variables
model: "data/models/polling.8.prism"
const: "T=16"
property_file: "data/properties/polling.props"
property_file: "data/models/polling.props"
property: "s1_before_s2"
expected: "0.5405549556"
heuristics: WEIGHTED
......
......@@ -3,17 +3,16 @@ Set-up Instructions
1. Clone the repository
2. Run `git submodule update --init` to populate `lib/prism`
3. Run `make` in `lib/prism/prism`
4. Run `./gradlew compileJava` to create the prism.jar and run the annotation processor
5. Import project in IntelliJ, enable gradle auto-import
3. Run `make` in `lib/prism/prism` to compile prism
Note: `./gradlew compileJava` has to be run whenever some of the annotation processor classes is changed.
Users:
Example Configurations
======================
Run `./gradlew distZip` to build and package the tool.
The package can be found under `build/distributions/`
Developers:
* `-m rabin3.nm --unbounded`
* `-m wlan4.nm --const k=0,TRANS_TIME_MAX=10 --bounded 100 --heuristic PROB`
* `-m cyclin.sm --const N=4 --bounded 100 --uniformization 30 --heuristic WEIGHTED`
* `-m zeroconf.nm --const N=1000,K=1000,err=0.01,reset=false --unbounded`
\ No newline at end of file
1. Import project in IntelliJ, enable gradle auto-import
2. Run `./gradlew compileJava` to create the prism.jar and run the annotation processor
Note: `./gradlew compileJava` has to be run whenever some of the annotation processor classes is changed.
\ No newline at end of file
......@@ -38,7 +38,7 @@ module plane
[] place=5 -> (1-crash) : (place'=6) + crash : (place'=8);
[] place=5 -> (place'=8);
t
[] place=6 & state=0 -> (1-flip) : (place'=7) + flip : (state'=1);
[] place=7 -> (1-crash) : (place'=0) + crash : (place'=8);
......@@ -53,3 +53,7 @@ module plane
[] state=1 -> 0.5 : (internal_2'=max(0, internal_2-1)) + 0.5 : (internal_2'=min(recovery_size, internal_2 + 1));
endmodule
rewards "default"
place=4 : 5;
place=8 : -10;
endrewards
const double crash;
mdp
module plane
// 0 munich
// 1 starting
// 2 mid-air
// 3 landing
// 4 prague
// 5 starting
// 6 mid-air
// 7 landing
// 8 crashed
place: [0..8];
[] place=0 -> 1 : (place'=1);
[] place=0 -> 1 : (place'=0);
[] place=1 -> (1-crash) : (place'=2) + crash : (place'=8);
[] place=1 -> 1 : (place'=8);
[] place=2 -> 1 : (place'=3);
[] place=3 -> (1-crash) : (place'=4) + crash : (place'=8);
[] place=3 -> 1 : (place'=8);
[] place=4 -> 1 : (place'=5);
[] place=4 -> 1 : (place'=4);
[] place=5 -> (1-crash) : (place'=6) + crash : (place'=8);
[] place=5 -> (place'=8);
[] place=6 -> 1 : (place'=7);
[] place=7 -> (1-crash) : (place'=0) + crash : (place'=8);
[] place=7 -> (place'=8);
[] place=8 -> (place'=8);
endmodule
rewards "default"
place=4 : 5;
place=0 : 1;
place=8 : -10;
endrewards
mdp
module server
s:[0..3];
i:[0..3];
j:[0..3];
// initial cancel loops
[client1_cancel] s=0 -> true;
[client2_cancel] s=0 -> true;
[client3_cancel] s=0 -> true;
// client i request/grant/cancel
[client1_request] s=0 -> (s'=1) & (i'=1);
[client1_grant] s=1 & i=1 -> (s'=2);
[client1_cancel] s=2 & i=1 -> (s'=0) & (i'=0);
[client2_request] s=0 -> (s'=1) & (i'=2);
[client2_grant] s=1 & i=2 -> (s'=2);
[client2_cancel] s=2 & i=2 -> (s'=0) & (i'=0);
[client3_request] s=0 -> (s'=1) & (i'=3);
[client3_grant] s=1 & i=3 -> (s'=2);
[client3_cancel] s=2 & i=3 -> (s'=0) & (i'=0);
// deny other requests when serving
[client1_request] s=2 -> (s'=3) & (j'=1);
[client1_deny] s=3 & j=1 -> (s'=2) & (j'=0);
[client2_request] s=2 -> (s'=3) & (j'=2);
[client2_deny] s=3 & j=2 -> (s'=2) & (j'=0);
[client3_request] s=2 -> (s'=3) & (j'=3);
[client3_deny] s=3 & j=3 -> (s'=2) & (j'=0);
// cancel loops when serving
[client1_cancel] s=2 & i!=1 -> true;
[client2_cancel] s=2 & i!=2 -> true;
[client3_cancel] s=2 & i!=3 -> true;
endmodule
module client1
c1:[-1..3];
[client1_ch_mind] c1=-1 -> 0.9:(c1'=0)+0.1:(c1'=3);
// change mind with probability 0.1
[client1_request] c1=0 -> (c1'=1);
[client1_deny] c1=1 -> (c1'=0);
[client1_grant] c1=1 -> (c1'=2);
[client1_useResource] c1=2 -> (c1'=2);
[client1_cancel] c1=2 -> (c1'=0);
[client1_cancel] c1=3 -> (c1'=1);
endmodule
module client2 = client1[ c1=c2, client1_ch_mind=client2_ch_mind, client1_request=client2_request,
client1_deny=client2_deny, client1_grant=client2_grant,
client1_useResource=client2_useResource, client1_cancel=client2_cancel]
endmodule
module client3 = client1[ c1=c3, client1_ch_mind=client3_ch_mind, client1_request=client3_request,
client1_deny=client3_deny, client1_grant=client3_grant,
client1_useResource=client3_useResource, client1_cancel=client3_cancel]
endmodule
rewards "grants"
[client1_grant] true : 1;
[client2_grant] true : 1;
[client3_grant] true : 1;
endrewards
\ No newline at end of file
......@@ -69,7 +69,7 @@ endrewards
module goldcounter
required_gold : [0..GOLD_TO_COLLECT] init GOLD_TO_COLLECT;
[right] true -> (required_gold'=max(0, required_gold - (left_of_home & gold ? 1: 0)));
[left] true -> (required_gold'=max(0, required_gold - (right_of_home & gold ? 1 : 0)));
[top] true -> (required_gold'=max(0, required_gold - (below_of_home & gold ? 1 : 0)));
......
......@@ -36,27 +36,27 @@ formula busy = c1>0 | c2>0;
formula free = c1=0 & c2=0;
module medium
// number of collisions
col : [0..COL+1];
// medium status
// medium status
c1 : [0..2];
c2 : [0..2];
// ci corresponds to messages associated with station i
// 0 nothing being sent
// 1 being sent correctly
// 2 being sent garbled
// 2 being sent garbled
// begin sending message and nothing else currently being sent
[send1] c1=0 & c2=0 -> (c1'=1);
[send2] c2=0 & c1=0 -> (c2'=1);
// begin sending message and something is already being sent
// in this case both messages become garbled
[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
// finish sending message
[finish1] c1>0 -> (c1'=0);
[finish2] c2>0 -> (c2'=0);
......@@ -68,26 +68,26 @@ endmodule
module station1
// clock for station 1
x1 : [0..TIME_MAX];
// local state
s1 : [1..12];
// 1 sense
// 2 wait until free before setting backoff
// 3 wait for DIFS then set slot
// 4 set backoff
// 4 set backoff
// 5 backoff
// 6 wait until free in backoff
// 7 wait for DIFS then resume backoff
// 8 vulnerable
// 8 vulnerable
// 9 transmit
// 11 wait for SIFS and then ACK
// 10 wait for ACT_TO
// 10 wait for ACT_TO
// 12 done
// BACKOFF
// separate into slots
slot1 : [0..63];
slot1 : [0..63];
backoff1 : [0..15];
// BACKOFF COUNTER
bc1 : [0..MAX_BACKOFF];
// SENSE
......@@ -177,7 +177,7 @@ module station1
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF))
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF))
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,MAX_BACKOFF));
// backoff counter 6
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=6 -> 1/64 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
......@@ -265,9 +265,9 @@ module station1
// let time pass
[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
......@@ -276,7 +276,7 @@ module station1
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
......@@ -284,7 +284,7 @@ module station1
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
......@@ -293,12 +293,12 @@ module station1
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
......@@ -309,13 +309,13 @@ module station1
// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
......@@ -325,24 +325,24 @@ module station1
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
......
This diff is collapsed.
......@@ -555,7 +555,7 @@ public final class CoreChecker {
ModelCheckerResult result = computeFringeReachability(mc, partialModel, stepBound);
double reachability = result.soln[initialState];
logger.log(Level.INFO, () -> String.format("Reachability: %f", reachability));
if (!Util.doublesAreLessOrEqual(reachability, precision)) {
if (!Util.lessOrEqual(reachability, precision)) {
throw new PrismException("Core property violated!");
}
}
......
......@@ -23,7 +23,7 @@ public class StateUpdateBoundedCore implements StateUpdateBounded, ValueVerdict
public Bounds update(int state, int remainingSteps, List<Distribution> choices,
StateValuesBoundedFunction values) {
if (choices.isEmpty()) {
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
double maximalValue = 0.0d;
......@@ -34,6 +34,6 @@ public class StateUpdateBoundedCore implements StateUpdateBounded, ValueVerdict
}
}
return Bounds.of(0.0d, maximalValue);
return Bounds.reach(0.0d, maximalValue);
}
}
......@@ -18,7 +18,7 @@ public class StateUpdateCore implements StateUpdate, ValueVerdict {
@Override
public Bounds update(int state, List<Distribution> choices, StateValueFunction values) {
if (choices.isEmpty()) {
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
double maximalValue = 0d;
......@@ -29,7 +29,7 @@ public class StateUpdateCore implements StateUpdate, ValueVerdict {
}
}
return Bounds.of(0.0d, maximalValue);
return Bounds.reach(0.0d, maximalValue);
}
@Override
......
......@@ -72,7 +72,7 @@ public class StateValuesBoundedCoreDense extends StateValuesBoundedCoreAbstract
} else {
double oldValue = values[remainingSteps];
// Check monotonicity of added value
assert Util.doublesAreLessOrEqual(value, oldValue) : "Updating " + oldValue + " to " + value;
assert Util.lessOrEqual(value, oldValue) : "Updating " + oldValue + " to " + value;
if (PrismUtils.doublesAreEqual(value, oldValue)) {
return;
}
......
......@@ -22,7 +22,7 @@ public class StateValuesUnboundedCore implements StateValues {
@Override
public Bounds bounds(int state) {
double upperBound = upperBound(state);
return upperBound == 0.0d ? Bounds.ZERO_ZERO : Bounds.of(0.0d, upperBound);
return upperBound == 0.0d ? Bounds.reachZero() : Bounds.reach(0.0d, upperBound);
}
......@@ -70,7 +70,7 @@ public class StateValuesUnboundedCore implements StateValues {
}
double oldValue = bounds.put(state, value);
assert Util.doublesAreLessOrEqual(value, oldValue) : "Value " + String.format("%.6g", value)
assert Util.lessOrEqual(value, oldValue) : "Value " + String.format("%.6g", value)
+ " larger than old value " + String.format("%.6g", oldValue);
}
......
......@@ -22,15 +22,15 @@ public class ReachabilityBounds {
// State was not known before
if (target.test(state)) {
oneStates.set(state);
return Bounds.ONE_ONE;
return Bounds.reachOne();
}
return null;
}
if (oneStates.contains(state)) {
return Bounds.ONE_ONE;
return Bounds.reachOne();
}
if (zeroStates.contains(state)) {
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
return null;
}
......
......@@ -23,16 +23,16 @@ public class StateUpdateBoundedReachability implements StateUpdateBounded {
if (values.lowerBound(state, remainingSteps) == 1.0d) {
assert values.upperBound(state, remainingSteps) == 1.0d;
return Bounds.ONE_ONE;
return Bounds.reachOne();
}
if (values.upperBound(state, remainingSteps) == 0.0d) {
assert values.lowerBound(state, remainingSteps) == 0.0d;
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
assert !target.test(state);
if (choices.isEmpty()) {
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
if (choices.size() == 1) {
......
......@@ -26,16 +26,16 @@ public class StateUpdateReachability implements StateUpdate {
if (values.lowerBound(state) == 1.0d) {
assert values.upperBound(state) == 1.0d;
return Bounds.ONE_ONE;
return Bounds.reachOne();
}
if (values.upperBound(state) == 0.0d) {
assert values.lowerBound(state) == 0.0d;
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
assert !target.test(state);
if (choices.isEmpty()) {
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
if (choices.size() == 1) {
return values.bounds(state, choices.get(0));
......@@ -89,7 +89,7 @@ public class StateUpdateReachability implements StateUpdate {
while (iterator.hasNext()) {
int next = iterator.nextInt();
if (target.test(next)) {
return Bounds.ONE_ONE;
return Bounds.reachOne();
}
}
return update(state, choices, values);
......
......@@ -27,21 +27,21 @@ public class StateValuesBoundedReachability implements StateValuesBounded {
}
if (remainingSteps == 0) {
// State is not a special reachability state
return Bounds.ZERO_ZERO;
return Bounds.reachZero();
}
Bounds[] values = bounds.get(state);
if (values == null) {
return Bounds.ZERO_ONE;
return Bounds.reachUnknown();
}
return remainingSteps < values.length ? values[remainingSteps] : Bounds.ZERO_ONE;
return remainingSteps < values.length ? values[remainingSteps] : Bounds.reachUnknown();
}
@Override
public void setBounds(int state, int remainingSteps, double lowerBound, double upperBound) {
checkArgument(0 <= remainingSteps);
Bounds bounds = Bounds.of(lowerBound, upperBound);
Bounds bounds = Bounds.reach(lowerBound, upperBound);
Bounds[] values = this.bounds.get(state);
if (values == null) {
......@@ -55,7 +55,7 @@ public class StateValuesBoundedReachability implements StateValuesBounded {
int newLength = Math.max(oldLength * 2, remainingSteps + 1);
values = Arrays.copyOf(values, newLength);
Arrays.fill(values, oldLength, remainingSteps + 1, bounds);
Arrays.fill(values, remainingSteps + 1, newLength, Bounds.ZERO_ONE);
Arrays.fill(values, remainingSteps + 1, newLength, Bounds.reachUnknown());
this.bounds.put(state, values);
return;
}
......
......@@ -23,15 +23,20 @@ public class StateValuesReachability implements StateValues {
return reachabilityBounds;
}
Bounds storedBounds = this.bounds.get(state);
return storedBounds == null ? Bounds.ZERO_ONE : storedBounds;
return storedBounds == null ? Bounds.reachUnknown() : storedBounds;
}
@Override
public Bounds bounds(int state, Distribution distribution) {
return Bounds.reach(lowerBound(state, distribution), upperBound(state, distribution));
}
@Override
public void setBounds(int state, double lowerBound, double upperBound) {
assert 0 <= lowerBound && lowerBound <= upperBound && upperBound <= 1.0d;
assert reachability.isKnown(state);
assert Util.doublesAreLessOrEqual(lowerBound(state), lowerBound)
&& Util.doublesAreLessOrEqual(upperBound, upperBound(state));
assert Util.lessOrEqual(lowerBound(state), lowerBound)
&& Util.lessOrEqual(upperBound, upperBound(state));
if (reachability.set(state, lowerBound, upperBound)) {
bounds.remove(state);
......
......@@ -11,7 +11,6 @@ import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.function.Consumer;
import javax.annotation.Nullable;
import prism.ModelType;
import prism.PrismLog;
import strat.MDStrategy;
......@@ -133,7 +132,7 @@ public class MDP extends DefaultModel implements explicit.MDP, NondetModelSimple
@Override
public List<Action> getActions(int state) {
return transitions.get(state);
return transitions.getOrDefault(state, Collections.emptyList());
}
@Override
......@@ -142,7 +141,6 @@ public class MDP extends DefaultModel implements explicit.MDP, NondetModelSimple
}
@Override
@Nullable
public List<Distribution> getChoices(int state) {
List<Action> actions = transitions.get(state);
if (actions == null) {
......
......@@ -28,9 +28,12 @@ public final class PrismHelper {
private PrismHelper() {}
public static PrismParseResult parse(CommandLine commandLine, Option modelOption,
Option propertiesOption, Option constantsOption) throws IOException, PrismException {
@Nullable Option propertiesOption, Option constantsOption)
throws IOException, PrismException {
String modelPath = commandLine.getOptionValue(modelOption.getLongOpt());
String propertiesPath = commandLine.getOptionValue(propertiesOption.getLongOpt());
@Nullable
String propertiesPath = propertiesOption == null
? null : commandLine.getOptionValue(propertiesOption.getLongOpt());
@Nullable
String constantsString = commandLine.hasOption(constantsOption.getLongOpt())
? commandLine.getOptionValue(constantsOption.getLongOpt())
......
......@@ -31,12 +31,14 @@ import java.util.Arrays;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.function.IntFunction;
import java.util.function.IntPredicate;
import java.util.function.IntToDoubleFunction;
import java.util.function.ToDoubleFunction;
public final class Util {
public static final double DEFAULT_PRECISION = 1e-6;
private static final double MACHINE_EPS = 1e-12;
private Util() {}
......@@ -188,6 +190,76 @@ public final class Util {
return foundBitSets;
}
public static void modelToDotFile(String filename, Model model, IntFunction<Object> label,
IntPredicate stateFilter, IntPredicate highlight) {
StringBuilder dotString = new StringBuilder("digraph Model {\n\tnode [shape=box];\n");
for (int state = 0; state < model.getNumStates(); state++) {
if (!stateFilter.test(state)) {
continue;
}
dotString.append(state).append(" [style=filled fillcolor=\"");
if (highlight != null && highlight.test(state)) {
dotString.append("#22CC22");
} else if (model.isInitialState(state)) {
dotString.append("#9999CC");
} else {
dotString.append("#DDDDDD");
}
dotString.append("\",label=\"").append(state);
Object stateLabel = label.apply(state);
if (stateLabel != null) {
dotString.append(' ').append(stateLabel);
}
dotString.append("\"];\n");
int actionIndex = 0;
for (Action action : model.getActions(state)) {
Object actionLabel = action.label();
if (action.distribution().size() == 1) {
IntIterator iterator = action.distribution().support().iterator();
int successor = iterator.nextInt();
assert !iterator.hasNext();
dotString.append(state).append(" -> ").append(successor);
if (actionLabel != null) {
dotString.append("[label=\"").append(actionLabel).append("\"]");
}
dotString.append(";\n");
} else {
String actionNode = "a" + state + '_' + actionIndex;
dotString.append(state).append(" -> ").append(actionNode)
.append(" [arrowhead=none,label=\"").append(actionIndex);
if (actionLabel != null) {
dotString.append(':').append(actionLabel);
}
dotString.append("\" ];\n");
dotString.append(actionNode).append(" [shape=point,height=0.1];\n");
action.distribution().forEach((target, probability) -> {
dotString.append(actionNode).append(" -> ").append(target);
if (!doublesAreEqual(probability, 1.0d)) {
dotString.append(" [label=\"").append(String.format("%.3f", probability))
.append("\"]");
}
dotString.append(";\n");
});
}
actionIndex += 1;
}
}
dotString.append("}\n");
try (BufferedWriter writer = Files.newBufferedWriter(Paths.get(filename),
StandardCharsets.UTF_8)) {
writer.append(dotString.toString());
} catch (IOException e) {
throw new AssertionError(e);
}
}
public static void modelWithBoundsToDotFile(String filename,
Model model, Explorer<?, ?> explorer, StateValueFunction values, IntPredicate stateFilter,
IntPredicate highlight) {
......@@ -338,7 +410,11 @@ public final class Util {
// CSON: Indentation
}
public static boolean doublesAreLessOrEqual(double d1, double d2) {
return d1 <= d2 || doublesAreEqual(d1, d2);
public static boolean equal(double d1, double d2) {
return Math.abs(d1 - d2) < MACHINE_EPS;
}
public static boolean lessOrEqual(double d1, double d2) {
return d1 <= d2 || equal(d1, d2);
}
}
package de.tum.in.pet.values;
import de.tum.in.pet.util.annotation.Tuple;
import org.immutables.value.Value;
import prism.PrismUtils;
@Value.Immutable
@Tuple
public abstract class Bounds {
public static final Bounds ZERO_ZERO;
public static final Bounds ZERO_ONE;
public static final Bounds ONE_ONE;
static {
ZERO_ZERO = BoundsTuple.create(0.0d, 0.0d);
ZERO_ONE = BoundsTuple.create(0.0d, 1.0d);
ONE_ONE = BoundsTuple.create(1.0d, 1.0d);
public static Bounds of(double lower, double upper) {
if (lower == upper) {
return of(lower);
}
return ValueBoundsTuple.create(lower, upper);
}
public static Bounds of(double value) {
return ValueBoundsTuple.create(value, value);
}
public abstract double lowerBound();
public abstract double upperBound();
public static Bounds unknown() {
return ValueBounds.UNKNOWN;
}
public static Bounds of(double lower, double upper) {
public static Bounds reach(double lower, double upper) {
if (lower == upper) {
return of(lower);
}
if (lower == 0.0d && upper == 1.0d) {
return ZERO_ONE;
return reachUnknown();
}
return BoundsTuple.create(lower, upper);
return ReachabilityBoundsTuple.create(lower, upper);
}
public static Bounds of(double value) {
public static Bounds reach(double value) {
if (value == 0.0d) {
return ZERO_ZERO;
return reachZero();
}
if (value == 1.0d) {
return ONE_ONE;
return reachOne();
}
return BoundsTuple.create(value, value);
return ReachabilityBoundsTuple.create(value, value);
}
public static Bounds reachZero() {
return ReachabilityBounds.ZERO;
}
@Override
public String toString() {
if (lowerBound() == 0.0d && upperBound() == 1.0d) {
return "[?]";
}
if (lowerBound() == upperBound()) {
return String.format("=%.5g", lowerBound());
}
if (lowerBound() == 0.0d) {
return String.format("<%.5g", upperBound());
}
if (upperBound() == 1.0d) {
return String.format(">%.5g", lowerBound());
}
public static Bounds reachOne() {
return ReachabilityBounds.ONE;
}
return String.format("[%.5g,%.5g]", lowerBound(), upperBound());
public static Bounds reachUnknown() {
return ReachabilityBounds.UNKNOWN;
}
public abstract double lowerBound();
public abstract double upperBound();
public double difference() {
assert upperBound() >= lowerBound();
return upperBound() - lowerBound();
}
......@@ -82,13 +76,9 @@ public abstract class Bounds {
}
public Bounds withUpper(double upperBound) {
return of(lowerBound(), upperBound);
}
public abstract Bounds withUpper(double upperBound);
public Bounds withLower(double lowerBound) {
return of(lowerBound, upperBound());
}
public abstract Bounds withLower(double lowerBound);
@Value.Check
......
package de.tum.in.pet.values;
import de.tum.in.pet.util.annotation.Tuple;
import org.immutables.value.Value;
@Value.Immutable
@Tuple
abstract class ReachabilityBounds extends Bounds {
static final ReachabilityBounds ZERO;
static final ReachabilityBounds UNKNOWN;
static final ReachabilityBounds ONE;
static {
ZERO = ReachabilityBoundsTuple.create(0.0d, 0.0d);
UNKNOWN = ReachabilityBoundsTuple.create(0.0d, 1.0d);
ONE = ReachabilityBoundsTuple.create(1.0d, 1.0d);
}
@Override
public Bounds withUpper(double upperBound) {
return of(lowerBound(), upperBound);
}
@Override
public Bounds withLower(double lowerBound) {
return of(lowerBound, upperBound());
}
@Override
public String toString() {
if (lowerBound() == 0.0d && upperBound() == 1.0d) {
return "[?]";
}
if (lowerBound() == upperBound()) {
return String.format("=%.5g", lowerBound());
}
if (lowerBound() == 0.0d) {
return String.format("<%.5g", upperBound());
}
if (upperBound() == 1.0d) {
return String.format(">%.5g", lowerBound());
}
return String.format("[%.5g,%.5g]", lowerBound(), upperBound());
}
@Override
protected void check() {
super.check();
assert 0.0d <= lowerBound() && upperBound() <= 1.0d;
}
}
package de.tum.in.pet.values;
import de.tum.in.pet.util.annotation.Tuple;
import org.immutables.value.Value;
@Value.Immutable
@Tuple
abstract class ValueBounds extends Bounds {
static final Bounds UNKNOWN;
static {
UNKNOWN = ValueBoundsTuple.of(Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY);
}
@Override
public Bounds withUpper(double upperBound) {
return of(lowerBound(), upperBound);
}
@Override
public Bounds withLower(double lowerBound) {
return of(lowerBound, upperBound());
}
@Override
public String toString() {
return lowerBound() == upperBound()
? String.format("=%.5g", lowerBound())
: String.format("[%.5g,%.5g]", lowerBound(), upperBound());
}
}