Importing Strategies for Model Checking

[Andy Hammer]

I want to utilize PRISM in such a way that I can model-check (or compute probabilities) for properties when utilizing a strategy for different inputs to the same model.

For example, this is my minimal working example.

mdp
const bool canPM2;
module main
num : [0..9] init 0;
tf : bool init true;
[addOne] (num < 9)
-> 0.5 : (num' = num+1)
 + 0.5 : true;
[minusOne] (num > 0)
-> 0.5 : (num' = num-1)
 + 0.5 : true;
[addTwo] (num < 7 & canPM2)
-> 0.5 : (num' = num+2)
 + 0.5 : true;
[minusTwo] (num > 2 & canPM2)
-> 0.5 : (num' = num-2)
 + 0.5 : true;
[flip] (true)
-> 0.5 : (tf' = !tf)
 + 0.5 : true;
endmodule
label "even" = mod(num, 2) = 0;

The property I am synthesizing a strategy for is Pmax=? [ G (!tf | "even") ] with input of canPM2=false. However, I want to compute P=? [ G (!tf | "even") ]  with the synthesized strategy for an input of canPM2=true.

I have been unable to simulate or compute probabilities for a model that has the same state space as a strategy, but does not have the same transitions. Is there anyway that I am able to do this?