How to make a pareto graph in PRISM games?

[Arsalaan Ahmed Khan]

Hi. 

I am trying to model an attack defense tree in PRISM games. I wish for PRISM to generate a pareto graph which will display the defense costs and the attack costs. However, I cannot find a property to do so. The "multi" property apparently does not work for stochastic mulitplayer games (smg). 

Also , how can I make it that one player tries to maximize the cost of the other? I want the defender to try to maximize attacker cost but how can I model that in PRISM? Some suggestions would be appreciated.

Also, in the manual it says that actions without a name are executed automatically, but when I simulate my model, I still have to click them to continue. I want the actions called "[]"(empty guards) to be executed automatically. So if the condition is true just execute them. But that does not seem to be the case. 

Here's my PRISM code : 
smg
// Define players
player defender
    [activate_D1], [activate_D2],[finish_setup_d], defend
endplayer

player attacker
     [execute_A1], [execute_A2], [execute_A3], attack
endplayer

// State variables
// 0: not executed, 1: executed or activated
// A1, A2, A3 represent attack states
// D1, D2, D3 represent defense states

global A1 : [0..1] init 0;
global A2 : [0..1] init 0;
global A3 : [0..1] init 0;

global D1 : [0..1] init 0;
global D2 : [0..1] init 0;
global D3 : [0..1] init 0;
global I1 : [0..1] init 0;
global I2 : [0..1] init 0;
global turn : [0..2] init 0;
global success_root : bool init false;
global r : [-2..2] init 0;
global total_costs_attacker : [0..100] init 0;
global total_costs_defender : [0..100] init 0;
global game_over : bool init false; // New state variable


module defend
    [activate_D1] turn=0 & D1=0 -> (D1' = 1) & (total_costs_defender' = total_costs_defender + 5);
    [activate_D2] turn=0 & D2=0 -> (D2' = 1) & (total_costs_defender' = total_costs_defender + 10);
    [] turn=0 & D1=1 & D2=1 &D3=0 -> (D3' = 1);
    [finish_setup_d] turn=0 -> (turn' = 1);
endmodule

module attack
    [execute_A1] turn=1 & A1=0 & I1=0 & !game_over -> (A1' = 1) & (total_costs_attacker' = total_costs_attacker + 5) ;
    [execute_A2] turn=1 & A2=0 & !game_over -> (A2' = 1) & (total_costs_attacker' = total_costs_attacker + 10);
    [execute_A3] turn=1 & A3=0 & !game_over -> (A3' = 1) & (total_costs_attacker' = total_costs_attacker + 20);

    [] turn=1 & A1=0 & D3=1 & !game_over  & I1=0 -> (I1' = 1); //Handle INH1 gate
    [] turn=1 & A2=1 & I1=0 & !game_over & I2=0 -> (I2' = 1); //Handle INH2 gate
    [] turn=1 & (A3 = 1 | I2 = 1) & !game_over -> (success_root' = true) & (r' = 2) & (game_over' = true); // Attacker wins
    [] turn=1 & success_root = false & (A3 = 0 & I2 = 0) & !game_over -> (r' = -2) & (game_over' = true); //Defender wins
   
endmodule


// Cost structures
rewards "defender_costs"
    [activate_D1] true : 5;
    [activate_D2] true : 10;
    [finish_setup_d] true : 0;
endrewards

rewards "attacker_costs"
    [execute_A1] true : 5;
    [execute_A2] true : 10;
    [execute_A3] true : 20;
endrewards



// Define winning conditions
label "defender_wins" = r=-2;
label "attacker_wins" = r=2;

[Dave Parker]

Hi Arsalaan

> I am trying to model an attack defense tree in PRISM games. I wish for
> PRISM to generate a pareto graph which will display the defense costs
> and the attack costs. However, I cannot find a property to do so. The
> "multi" property apparently does not work for stochastic mulitplayer
> games (smg).

Yes, the format is a bit different for games. You have to add bounds.
Try a property like:

<<1>> (R{"defender_costs"}<=1 [ C ] & R{"attacker_costs"}<=1 [ C ])

and then click "Compute Pareto set" in the GUI menu, or add switch
-pareto from the command-line.

> Also , how can I make it that one player tries to maximize the cost of
> the other? I want the defender to try to maximize attacker cost but how
> can I model that in PRISM? Some suggestions would be appreciated.

You can change whether a cost is minimised or maximised by chnaging the
direction of the bound (<=1) in the property above.

> Also, in the manual it says that actions without a name are executed
> automatically, but when I simulate my model, I still have to click them
> to continue. I want the actions called "[]"(empty guards) to be executed
> automatically. So if the condition is true just execute them. But that
> does not seem to be the case.

I'm not sure what you mean by this. But, in the PRISM language, if two
command have their guards enabled, either can happen - one does not have
precedence over the other.

Best wishes,

Dave