{
  "jani-version": 1,
  "name": "Security/KSA22/KSA22_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": "app_Evt"
    },
    {
      "name": "switch_switch_1_GarageDoorOpener0_0"
    },
    {
      "name": "switch_switch_Evt_1"
    },
    {
      "name": "delay_18_2_sync"
    },
    {
      "name": "switch_switch_1_automata_delay_18_2_sync_0"
    },
    {
      "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": "clock_GarageDoorOpener_0",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "app_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "app",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "switch_switch_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "delta",
      "type": "real",
      "initial-value": 5
    },
    {
      "name": "trigger_GarageDoorOpener",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "delay",
      "type": "real",
      "initial-value": 3
    }
  ],
  "properties": [],
  "automata": [
    {
      "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
                },
                {
                  "ref": "switch_switch_1_sensor_clk",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "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
                },
                {
                  "ref": "switch_switch_1_sensor_clk",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_GarageDoorOpener0_0",
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        }
      ]
    },
    {
      "name": "GarageDoorOpener0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "app_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_GarageDoorOpener0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 97
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "automata_delay_18_2_sync",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "delay",
              "right": "clock_GarageDoorOpener_0"
            }
          }
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "delay_18_2_sync",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "clock_GarageDoorOpener_0",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_automata_delay_18_2_sync_0",
          "guard": {
            "exp": {
              "op": ">",
              "left": "clock_GarageDoorOpener_0",
              "right": "delay"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                },
                {
                  "ref": "trigger_GarageDoorOpener",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "GarageDoorOpener1",
      "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_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_3",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_4",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "delay_18_2_sync",
          "guard": {
            "exp": {
              "op": "=",
              "left": "trigger_GarageDoorOpener",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "trigger_GarageDoorOpener",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_5",
          "guard": {
            "exp": {
              "op": "=",
              "left": "trigger_GarageDoorOpener",
              "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_automata_delay_18_2_sync_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_GarageDoorOpener0_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_6",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_7",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_8",
          "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_automata_delay_18_2_sync_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "delta",
              "right": "timer_switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "switch_switch_1_GarageDoorOpener0_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_9",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode2"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_10",
          "guard": {
            "exp": {
              "op": "<",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_11",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "app_Env"
      },
      {
        "automaton": "switch_switch_Dev_1"
      },
      {
        "automaton": "GarageDoorOpener0"
      },
      {
        "automaton": "automata_delay_18_2_sync"
      },
      {
        "automaton": "GarageDoorOpener1"
      },
      {
        "automaton": "switch_on_deadline_switch"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "app_Evt",
          null,
          "app_Evt",
          null,
          null,
          null
        ],
        "result": "app_Evt"
      },
      {
        "synchronise": [
          null,
          "switch_switch_1_GarageDoorOpener0_0",
          "switch_switch_1_GarageDoorOpener0_0",
          null,
          null,
          "switch_switch_1_GarageDoorOpener0_0"
        ],
        "result": "switch_switch_1_GarageDoorOpener0_0"
      },
      {
        "synchronise": [
          null,
          "switch_switch_Evt_1",
          null,
          null,
          "switch_switch_Evt_1",
          "switch_switch_Evt_1"
        ],
        "result": "switch_switch_Evt_1"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          "delay_18_2_sync",
          "delay_18_2_sync",
          null
        ],
        "result": "delay_18_2_sync"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          "switch_switch_1_automata_delay_18_2_sync_0",
          null,
          "switch_switch_1_automata_delay_18_2_sync_0"
        ],
        "result": "switch_switch_1_automata_delay_18_2_sync_0"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          null,
          "badstate"
        ],
        "result": "badstate"
      }
    ]
  }
}