[mcsta] Compute explicit scheduler
When computing properties via probabilistic model checking in mcsta, modest computes an implicit optimal scheduler. It would be great if one could obtain this scheduler explicitly to compute some optimal paths (if the model does not contain probabilistic choices).
Example
action a, b; // nondeterminism between these two actions
clock time;
bool success; // flag indicating that we reached the success-state
bool increaseReward; // flag indicating if we currently accumulate reward 1 per edge
int n;
// the minimum/maximum probability that we reach the success-state within 20 time units
property succMin = Pmin (<>[T <= 20] success);
property succMax = Pmax (<>[T <= 20] success);
// the minimum/maximum expected accumulated reward until the success-state is reached
property stepsMin = Xmin(S(increaseReward ? 1 : 0), success);
property stepsMax = Xmax(S(increaseReward ? 1 : 0), success);
// the maximum/minimum time until we reach the success-state
property timeMin = Xmin(T, success);
property timeMax = Xmax(T, success);
process P() {
alt {
:: delay(1) a {= n += 1, increaseReward = true =}; urgent tau
:: delay(2) b {= n += 3, increaseReward = true =}; urgent tau; urgent tau; urgent tau
}; urgent tau {= increaseReward = false =};
alt {
:: when (n >= 10) urgent tau {= success = true =}
:: when (n < 10) urgent tau; P()
}
}
P()
1
Mosta representationProperties
The minimum / maximum probability that we reach the success-state within 20 time units.
+ Property succMin
Probability: 1
CDF: { (0, 0), ..., (19, 0), (20, 1) }
+ Property succMax
Probability: 1
CDF: { (0, 0), ..., (6, 0), (7, 1) }
- see both time properties below
The minimum expected accumulated reward until the success-state is reached.
+ Property stepsMin
Value: 14
- the scheduler should schedule three times the
b
-transition (accumulating reward four on each) in the initial state and choose thea
-transition only once (accumulating two)
The maximum expected accumulated reward until the success-state is reached.
+ Property stepsMax
Value: 22
- the scheduler should schedule nine times the
a
-transition (accumulating reward two on each) in the initial state and choose theb
-transition only once (accumulating four)
The minimum time until we reach the success-state.
+ Property timeMin
Value: 7
- the scheduler should schedule three times the
b
-transition (taking each two time units) in the initial state and choose thea
-transition only once (taking one time unit)
The maximum time until we reach the success-state.
+ Property timeMax
Value: 20
- the scheduler should always schedule the
a
-transition in the initial state but first waiting there for the full two time units
(I was a little bit confused about this behavior but did not succeed to combinedelay
andurgent
, e.g.delay(1) urgent a
)
Furthermore I did not succeed in declaring reward bounded properties.
-
I used
mosta
in the Modest Toolset,version 3.0 Beta 1
from the website because the currentmosta
in e2d1824dc041c50be3a94f50306ed9c99671f7da appends_instance_n
to all variables.↩