{
  "jani-version": 1,
  "name": "Train/train_intruder/train_intruder-4.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "sensor_far"
    },
    {
      "name": "sensor_close"
    },
    {
      "name": "pass"
    },
    {
      "name": "power_cut"
    },
    {
      "name": "start_lowering"
    },
    {
      "name": "end_lowering"
    },
    {
      "name": "break_sensor"
    },
    {
      "name": "choose_house"
    },
    {
      "name": "choose_sensor"
    }
  ],
  "variables": [
    {
      "name": "x_train",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "x_gate",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "x_intruder",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "gate_down",
      "type": "bool",
      "initial-value": false
    },
    {
      "name": "sensors_active",
      "type": "bool",
      "initial-value": true
    },
    {
      "name": "p_far",
      "type": "real"
    },
    {
      "name": "p_approaching",
      "type": "real"
    },
    {
      "name": "p_very_near",
      "type": "real"
    },
    {
      "name": "p_waiting",
      "type": "real"
    },
    {
      "name": "p_emergency_waiting",
      "type": "real"
    },
    {
      "name": "p_emergency_lowering",
      "type": "real"
    },
    {
      "name": "p_lowering",
      "type": "real"
    },
    {
      "name": "p_walking_sensor",
      "type": "real"
    },
    {
      "name": "p_walking_house",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "train",
      "locations": [
        {
          "name": "far",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_far",
              "right": "x_train"
            }
          }
        },
        {
          "name": "approaching",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_approaching",
              "right": {
                "op": "+",
                "left": "p_very_near",
                "right": "x_train"
              }
            }
          }
        },
        {
          "name": "very_near",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_approaching",
              "right": "x_train"
            }
          }
        },
        {
          "name": "gone",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 0,
              "right": "x_train"
            }
          }
        },
        {
          "name": "crash",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 0,
              "right": "x_train"
            }
          }
        }
      ],
      "initial-locations": [
        "far"
      ],
      "edges": [
        {
          "location": "far",
          "action": "sensor_far",
          "guard": {
            "exp": {
              "op": "∧",
              "left": "sensors_active",
              "right": {
                "op": "=",
                "left": "p_far",
                "right": "x_train"
              }
            }
          },
          "destinations": [
            {
              "location": "approaching",
              "assignments": [
                {
                  "ref": "x_train",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "far",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "¬",
                "exp": "sensors_active"
              },
              "right": {
                "op": "=",
                "left": "p_far",
                "right": "x_train"
              }
            }
          },
          "destinations": [
            {
              "location": "approaching",
              "assignments": [
                {
                  "ref": "x_train",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "approaching",
          "action": "sensor_close",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_approaching",
              "right": {
                "op": "+",
                "left": "p_very_near",
                "right": "x_train"
              }
            }
          },
          "destinations": [
            {
              "location": "very_near"
            }
          ]
        },
        {
          "location": "very_near",
          "action": "pass",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "¬",
                "exp": "gate_down"
              },
              "right": {
                "op": "=",
                "left": "p_approaching",
                "right": "x_train"
              }
            }
          },
          "destinations": [
            {
              "location": "crash",
              "assignments": [
                {
                  "ref": "x_train",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "very_near",
          "action": "pass",
          "guard": {
            "exp": {
              "op": "∧",
              "left": "gate_down",
              "right": {
                "op": "=",
                "left": "p_approaching",
                "right": "x_train"
              }
            }
          },
          "destinations": [
            {
              "location": "gone",
              "assignments": [
                {
                  "ref": "x_train",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "gate",
      "locations": [
        {
          "name": "up"
        },
        {
          "name": "no_power",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_emergency_waiting",
              "right": "x_gate"
            }
          }
        },
        {
          "name": "waiting",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_waiting",
              "right": "x_gate"
            }
          }
        },
        {
          "name": "lowering",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_lowering",
              "right": "x_gate"
            }
          }
        },
        {
          "name": "emergency_lowering",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_emergency_lowering",
              "right": "x_gate"
            }
          }
        },
        {
          "name": "down"
        }
      ],
      "initial-locations": [
        "up"
      ],
      "edges": [
        {
          "location": "up",
          "action": "sensor_far",
          "destinations": [
            {
              "location": "waiting",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "up",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "emergency_lowering",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "up",
          "action": "power_cut",
          "destinations": [
            {
              "location": "no_power",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "up",
          "action": "pass",
          "destinations": [
            {
              "location": "up",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "no_power",
          "action": "start_lowering",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_emergency_waiting",
              "right": "x_gate"
            }
          },
          "destinations": [
            {
              "location": "emergency_lowering",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "no_power",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "emergency_lowering",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "no_power",
          "action": "pass",
          "destinations": [
            {
              "location": "no_power",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "no_power",
          "action": "sensor_far",
          "destinations": [
            {
              "location": "no_power",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waiting",
          "action": "start_lowering",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_waiting",
              "right": "x_gate"
            }
          },
          "destinations": [
            {
              "location": "lowering",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waiting",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "emergency_lowering",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waiting",
          "action": "pass",
          "destinations": [
            {
              "location": "up",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waiting",
          "action": "power_cut",
          "destinations": [
            {
              "location": "no_power",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "lowering",
          "action": "end_lowering",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_lowering",
              "right": "x_gate"
            }
          },
          "destinations": [
            {
              "location": "down",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                },
                {
                  "ref": "gate_down",
                  "value": true
                }
              ]
            }
          ]
        },
        {
          "location": "lowering",
          "action": "power_cut",
          "destinations": [
            {
              "location": "lowering"
            }
          ]
        },
        {
          "location": "lowering",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "lowering"
            }
          ]
        },
        {
          "location": "lowering",
          "action": "pass",
          "destinations": [
            {
              "location": "up",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "emergency_lowering",
          "action": "end_lowering",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_emergency_lowering",
              "right": "x_gate"
            }
          },
          "destinations": [
            {
              "location": "down",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                },
                {
                  "ref": "gate_down",
                  "value": true
                }
              ]
            }
          ]
        },
        {
          "location": "emergency_lowering",
          "action": "pass",
          "destinations": [
            {
              "location": "up",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "emergency_lowering",
          "action": "power_cut",
          "destinations": [
            {
              "location": "emergency_lowering"
            }
          ]
        },
        {
          "location": "emergency_lowering",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "emergency_lowering"
            }
          ]
        },
        {
          "location": "down",
          "action": "pass",
          "destinations": [
            {
              "location": "up",
              "assignments": [
                {
                  "ref": "x_gate",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "down",
          "action": "power_cut",
          "destinations": [
            {
              "location": "down"
            }
          ]
        },
        {
          "location": "down",
          "action": "sensor_close",
          "destinations": [
            {
              "location": "down"
            }
          ]
        }
      ]
    },
    {
      "name": "intruder",
      "locations": [
        {
          "name": "choosing"
        },
        {
          "name": "walking_sensor",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_walking_sensor",
              "right": "x_intruder"
            }
          }
        },
        {
          "name": "walking_house",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_walking_house",
              "right": "x_intruder"
            }
          }
        },
        {
          "name": "intruder_done"
        }
      ],
      "initial-locations": [
        "choosing"
      ],
      "edges": [
        {
          "location": "choosing",
          "action": "choose_sensor",
          "destinations": [
            {
              "location": "walking_sensor"
            }
          ]
        },
        {
          "location": "choosing",
          "action": "choose_house",
          "destinations": [
            {
              "location": "walking_house"
            }
          ]
        },
        {
          "location": "walking_sensor",
          "action": "break_sensor",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_walking_sensor",
              "right": "x_intruder"
            }
          },
          "destinations": [
            {
              "location": "intruder_done",
              "assignments": [
                {
                  "ref": "sensors_active",
                  "value": false
                },
                {
                  "ref": "x_intruder",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "walking_house",
          "action": "power_cut",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_walking_house",
              "right": "x_intruder"
            }
          },
          "destinations": [
            {
              "location": "intruder_done",
              "assignments": [
                {
                  "ref": "sensors_active",
                  "value": false
                },
                {
                  "ref": "x_intruder",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "train"
      },
      {
        "automaton": "gate"
      },
      {
        "automaton": "intruder"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "sensor_far",
          "sensor_far",
          null
        ],
        "result": "sensor_far"
      },
      {
        "synchronise": [
          "sensor_close",
          "sensor_close",
          null
        ],
        "result": "sensor_close"
      },
      {
        "synchronise": [
          "pass",
          "pass",
          null
        ],
        "result": "pass"
      },
      {
        "synchronise": [
          null,
          "power_cut",
          "power_cut"
        ],
        "result": "power_cut"
      },
      {
        "synchronise": [
          null,
          "start_lowering",
          null
        ],
        "result": "start_lowering"
      },
      {
        "synchronise": [
          null,
          "end_lowering",
          null
        ],
        "result": "end_lowering"
      },
      {
        "synchronise": [
          null,
          null,
          "break_sensor"
        ],
        "result": "break_sensor"
      },
      {
        "synchronise": [
          null,
          null,
          "choose_house"
        ],
        "result": "choose_house"
      },
      {
        "synchronise": [
          null,
          null,
          "choose_sensor"
        ],
        "result": "choose_sensor"
      }
    ]
  }
}