phil3.jani

{
    "jani-version":1,
    "name":"phil3",
    "type":"mdp",
    "features":[
        "derived-operators"
    ],
    "actions":[
        {
            "name":"τ"
        }
    ],
    "constants":[
    ],
    "variables":[
        {
            "name":"p1",
            "type":{
                "kind":"bounded",
                "base":"int",
                "lower-bound":0,
                "upper-bound":11
            }
        },
        {
            "name":"p2",
            "type":{
                "kind":"bounded",
                "base":"int",
                "lower-bound":0,
                "upper-bound":11
            }
        },
        {
            "name":"p3",
            "type":{
                "kind":"bounded",
                "base":"int",
                "lower-bound":0,
                "upper-bound":11
            }
        }
    ],
    "restrict-initial":{
        "exp":{
            "op":"∧",
            "left":{
                "op":"∧",
                "left":{
                    "op":"=",
                    "left":"p1",
                    "right":0
                },
                "right":{
                    "op":"=",
                    "left":"p2",
                    "right":0
                }
            },
            "right":{
                "op":"=",
                "left":"p3",
                "right":0
            }
        }
    },
    "properties":[
        {
            "name":"Property_phil3_0",
            "expression":{
                "op":"filter",
                "fun":"∀",
                "values":{
                    "op":"⇒",
                    "left":{
                        "op":"∨",
                        "left":{
                            "op":"∨",
                            "left":{
                                "op":"∧",
                                "left":{
                                    "op":">",
                                    "left":"p1",
                                    "right":0
                                },
                                "right":{
                                    "op":"<",
                                    "left":"p1",
                                    "right":8
                                }
                            },
                            "right":{
                                "op":"∧",
                                "left":{
                                    "op":">",
                                    "left":"p2",
                                    "right":0
                                },
                                "right":{
                                    "op":"<",
                                    "left":"p2",
                                    "right":8
                                }
                            }
                        },
                        "right":{
                            "op":"∧",
                            "left":{
                                "op":">",
                                "left":"p3",
                                "right":0
                            },
                            "right":{
                                "op":"<",
                                "left":"p3",
                                "right":8
                            }
                        }
                    },
                    "right":{
                        "op":"≤",
                        "left":1,
                        "right":{
                            "op":"Pmin",
                            "exp":{
                                "op":"U",
                                "left":true,
                                "right":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p1",
                                                "right":8
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p1",
                                                "right":9
                                            }
                                        },
                                        "right":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p2",
                                                "right":8
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p2",
                                                "right":9
                                            }
                                        }
                                    },
                                    "right":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p3",
                                            "right":8
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p3",
                                            "right":9
                                        }
                                    }
                                }
                            }
                        }
                    }
                },
                "states":true
            },
            "comment":"filter(forall, \"hungry\" => P>=1 [ F \"eat\" ])"
        }
    ],
    "automata":[
        {
            "name":"phil1",
            "locations":[
                {
                    "name":"location"
                }
            ],
            "initial-locations":[
                "location"
            ],
            "edges":[
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":1
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":2
                                }
                            ]
                        },
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":2
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p2",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p2",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p2",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":4
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":2
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p2",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p2",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":2
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":3
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p3",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p3",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p3",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":5
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":3
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p3",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p3",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p3",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":4
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p3",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p3",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p3",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":4
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p3",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p3",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p3",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":6
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":5
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p2",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p2",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p2",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p1",
                                "right":5
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p2",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p2",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":7
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":6
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":7
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":8
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":9
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":10
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":11
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":10
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p1",
                            "right":11
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p1",
                                    "value":0
                                }
                            ]
                        }
                    ]
                }
            ]
        },
        {
            "name":"phil2",
            "locations":[
                {
                    "name":"location"
                }
            ],
            "initial-locations":[
                "location"
            ],
            "edges":[
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":1
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":2
                                }
                            ]
                        },
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":2
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p3",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p3",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p3",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":4
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":2
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p3",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p3",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":2
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":3
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p1",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p1",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p1",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":5
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":3
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p1",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p1",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p1",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":4
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p1",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p1",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p1",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":4
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p1",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p1",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p1",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":6
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":5
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p3",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p3",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p3",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p2",
                                "right":5
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p3",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p3",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p3",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p3",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":7
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":6
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":7
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":8
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":9
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":10
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":11
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":10
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p2",
                            "right":11
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p2",
                                    "value":0
                                }
                            ]
                        }
                    ]
                }
            ]
        },
        {
            "name":"phil3",
            "locations":[
                {
                    "name":"location"
                }
            ],
            "initial-locations":[
                "location"
            ],
            "edges":[
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":0
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":1
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":2
                                }
                            ]
                        },
                        {
                            "probability":{
                                "exp":0.5000000
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":2
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p1",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p1",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p1",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":4
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":2
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p1",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p1",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":2
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":3
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p2",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p2",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p2",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":5
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":3
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p2",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p2",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p2",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":3
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":4
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p2",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p2",
                                                "right":3
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":5
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":7
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p2",
                                    "right":11
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":4
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∨",
                                            "left":{
                                                "op":"∧",
                                                "left":{
                                                    "op":"≥",
                                                    "left":"p2",
                                                    "right":0
                                                },
                                                "right":{
                                                    "op":"≤",
                                                    "left":"p2",
                                                    "right":3
                                                }
                                            },
                                            "right":{
                                                "op":"=",
                                                "left":"p2",
                                                "right":5
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p2",
                                            "right":7
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p2",
                                        "right":11
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":6
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":5
                            },
                            "right":{
                                "op":"∨",
                                "left":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∧",
                                        "left":{
                                            "op":"≥",
                                            "left":"p1",
                                            "right":0
                                        },
                                        "right":{
                                            "op":"≤",
                                            "left":"p1",
                                            "right":4
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":6
                                    }
                                },
                                "right":{
                                    "op":"=",
                                    "left":"p1",
                                    "right":10
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":8
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"∧",
                            "left":{
                                "op":"=",
                                "left":"p3",
                                "right":5
                            },
                            "right":{
                                "op":"¬",
                                "exp":{
                                    "op":"∨",
                                    "left":{
                                        "op":"∨",
                                        "left":{
                                            "op":"∧",
                                            "left":{
                                                "op":"≥",
                                                "left":"p1",
                                                "right":0
                                            },
                                            "right":{
                                                "op":"≤",
                                                "left":"p1",
                                                "right":4
                                            }
                                        },
                                        "right":{
                                            "op":"=",
                                            "left":"p1",
                                            "right":6
                                        }
                                    },
                                    "right":{
                                        "op":"=",
                                        "left":"p1",
                                        "right":10
                                    }
                                }
                            }
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":7
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":6
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":7
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":1
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":8
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":9
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":10
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":9
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":11
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":10
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":0
                                }
                            ]
                        }
                    ]
                },
                {
                    "location":"location",
                    "action":"τ",
                    "guard":{
                        "exp":{
                            "op":"=",
                            "left":"p3",
                            "right":11
                        }
                    },
                    "destinations":[
                        {
                            "probability":{
                                "exp":1
                            },
                            "location":"location",
                            "assignments":[
                                {
                                    "ref":"p3",
                                    "value":0
                                }
                            ]
                        }
                    ]
                }
            ]
        }
    ],
    "system":{
        "elements":[
            {
                "automaton":"phil1"
            },
            {
                "automaton":"phil2"
            },
            {
                "automaton":"phil3"
            }
        ],
        "syncs":[
            {
                "synchronise":[
                    "τ",
                    null,
                    null
                ],
                "result":"τ"
            },
            {
                "synchronise":[
                    null,
                    "τ",
                    null
                ],
                "result":"τ"
            },
            {
                "synchronise":[
                    null,
                    null,
                    "τ"
                ],
                "result":"τ"
            }
        ]
    }
}