{
  "jani-version": 1,
  "name": "Security/KSA22/KSA22_5.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "location_Evt"
    },
    {
      "name": "app_Evt"
    },
    {
      "name": "switch_switch_1_automata_3_turnOffSwitch_0"
    },
    {
      "name": "switch_switch_Evt_1"
    },
    {
      "name": "switch_switch_1_BigTurnON0_0"
    },
    {
      "name": "switch_switch_1_BigTurnON1_0"
    },
    {
      "name": "runIn_turnOffSwitch_sync"
    },
    {
      "name": "badstate"
    }
  ],
  "variables": [
    {
      "name": "switch_switch_1_sensor_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "timer_switch_switch_1",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "clk_runIn_turnOffSwitch",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "app_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "location_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "app",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "location",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "switch_switch_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "trigger_turnOffSwitch",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "delta",
      "type": "real",
      "initial-value": 300
    },
    {
      "name": "minutesLater_3",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "location_Env",
      "locations": [
        {
          "name": "mode0"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "location_Evt",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "location_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "location",
                  "value": 1
                },
                {
                  "ref": "location_clk",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "location_Evt",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "location_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "location",
                  "value": 0
                },
                {
                  "ref": "location_clk",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "app_Env",
      "locations": [
        {
          "name": "mode0"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "app_Evt",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "app_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "app",
                  "value": 1
                },
                {
                  "ref": "app_clk",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "app_Evt",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "app_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "app",
                  "value": 0
                },
                {
                  "ref": "app_clk",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "switch_switch_Dev_1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "mode2"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "switch_switch_Evt_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1_sensor_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 97
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_Evt_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1_sensor_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnON1_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1_sensor_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnON0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1_sensor_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_automata_3_turnOffSwitch_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1_sensor_clk",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        }
      ]
    },
    {
      "name": "BigTurnON0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "location_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnON0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "location",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 97
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "location",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "BigTurnON1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "app_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnON1_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 97
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_2",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "automata_3_turnOffSwitch",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": {
                "op": "*",
                "left": 60,
                "right": "minutesLater_3"
              },
              "right": "clk_runIn_turnOffSwitch"
            }
          }
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "runIn_turnOffSwitch_sync",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "clk_runIn_turnOffSwitch",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_automata_3_turnOffSwitch_0",
          "guard": {
            "exp": {
              "op": ">",
              "left": "clk_runIn_turnOffSwitch",
              "right": {
                "op": "*",
                "left": 60,
                "right": "minutesLater_3"
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                },
                {
                  "ref": "trigger_turnOffSwitch",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "PowerAllowance0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "mode2"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "switch_switch_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_3",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_4",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_5",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "runIn_turnOffSwitch_sync",
          "guard": {
            "exp": {
              "op": "=",
              "left": "trigger_turnOffSwitch",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "trigger_turnOffSwitch",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_6",
          "guard": {
            "exp": {
              "op": "=",
              "left": "trigger_turnOffSwitch",
              "right": 1
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "switch_on_deadline_switch",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "mode2"
        },
        {
          "name": "mode3"
        },
        {
          "name": "conflict"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnON0_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnON1_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_automata_3_turnOffSwitch_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_7",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_8",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_9",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "badstate",
          "guard": {
            "exp": {
              "op": ">",
              "left": "timer_switch_switch_1",
              "right": "delta"
            }
          },
          "destinations": [
            {
              "location": "conflict"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_1_BigTurnON0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "delta",
              "right": "timer_switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_1_BigTurnON1_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "delta",
              "right": "timer_switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_1_automata_3_turnOffSwitch_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "delta",
              "right": "timer_switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_Evt_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "delta",
              "right": "timer_switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_10",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_11",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_12",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "location_Env"
      },
      {
        "automaton": "app_Env"
      },
      {
        "automaton": "switch_switch_Dev_1"
      },
      {
        "automaton": "BigTurnON0"
      },
      {
        "automaton": "BigTurnON1"
      },
      {
        "automaton": "automata_3_turnOffSwitch"
      },
      {
        "automaton": "PowerAllowance0"
      },
      {
        "automaton": "switch_on_deadline_switch"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "location_Evt",
          null,
          null,
          "location_Evt",
          null,
          null,
          null,
          null
        ],
        "result": "location_Evt"
      },
      {
        "synchronise": [
          null,
          "app_Evt",
          null,
          null,
          "app_Evt",
          null,
          null,
          null
        ],
        "result": "app_Evt"
      },
      {
        "synchronise": [
          null,
          null,
          "switch_switch_1_automata_3_turnOffSwitch_0",
          null,
          null,
          "switch_switch_1_automata_3_turnOffSwitch_0",
          null,
          "switch_switch_1_automata_3_turnOffSwitch_0"
        ],
        "result": "switch_switch_1_automata_3_turnOffSwitch_0"
      },
      {
        "synchronise": [
          null,
          null,
          "switch_switch_Evt_1",
          null,
          null,
          null,
          "switch_switch_Evt_1",
          "switch_switch_Evt_1"
        ],
        "result": "switch_switch_Evt_1"
      },
      {
        "synchronise": [
          null,
          null,
          "switch_switch_1_BigTurnON0_0",
          "switch_switch_1_BigTurnON0_0",
          null,
          null,
          null,
          "switch_switch_1_BigTurnON0_0"
        ],
        "result": "switch_switch_1_BigTurnON0_0"
      },
      {
        "synchronise": [
          null,
          null,
          "switch_switch_1_BigTurnON1_0",
          null,
          "switch_switch_1_BigTurnON1_0",
          null,
          null,
          "switch_switch_1_BigTurnON1_0"
        ],
        "result": "switch_switch_1_BigTurnON1_0"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          null,
          "runIn_turnOffSwitch_sync",
          "runIn_turnOffSwitch_sync",
          null
        ],
        "result": "runIn_turnOffSwitch_sync"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          null,
          null,
          null,
          "badstate"
        ],
        "result": "badstate"
      }
    ]
  }
}