{
  "jani-version": 1,
  "name": "Security/KSA22/KSA22_1.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": "PetFeederShield_off"
    },
    {
      "name": "PetFeederShield_on"
    },
    {
      "name": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0"
    },
    {
      "name": "switch_switch_1_BigTurnOFF0_0"
    },
    {
      "name": "switch_switch_1_BigTurnOFF1_0"
    }
  ],
  "variables": [
    {
      "name": "schedule_clock",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "timer_ba",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "location_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "app_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "location",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "app",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "switch_switch_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "time1_23",
      "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": "PetFeederShield_PetFeederShield_Dev_1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "PetFeederShield_off",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "PetFeederShield_on",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_off",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_on",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "PetFeederShield_PetFeederShield_Dev_interaction_1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnOFF0_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnOFF1_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_off",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 96
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_on",
          "guard": {
            "exp": {
              "op": "=",
              "left": "switch_switch_1",
              "right": 97
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "BigTurnOFF0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "location_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnOFF0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "location",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "location",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "BigTurnOFF1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "app_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnOFF1_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_2",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "app",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "FeedMyPet0",
      "locations": [
        {
          "name": "mode0",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "time1_23",
              "right": "schedule_clock"
            }
          }
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "guard": {
            "exp": {
              "op": "=",
              "left": "time1_23",
              "right": "schedule_clock"
            }
          },
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        }
      ]
    },
    {
      "name": "PetFeederShield_PetFeederShield_1_blocked_action",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "good"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnOFF0_0",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_ba",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_BigTurnOFF1_0",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "guard": {
            "exp": {
              "op": "=",
              "left": "timer_ba",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "timer_ba",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "good"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnOFF0_0",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_BigTurnOFF1_0",
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "location_Env"
      },
      {
        "automaton": "app_Env"
      },
      {
        "automaton": "PetFeederShield_PetFeederShield_Dev_1"
      },
      {
        "automaton": "PetFeederShield_PetFeederShield_Dev_interaction_1"
      },
      {
        "automaton": "BigTurnOFF0"
      },
      {
        "automaton": "BigTurnOFF1"
      },
      {
        "automaton": "FeedMyPet0"
      },
      {
        "automaton": "PetFeederShield_PetFeederShield_1_blocked_action"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "location_Evt",
          null,
          null,
          null,
          "location_Evt",
          null,
          null,
          null
        ],
        "result": "location_Evt"
      },
      {
        "synchronise": [
          null,
          "app_Evt",
          null,
          null,
          null,
          "app_Evt",
          null,
          null
        ],
        "result": "app_Evt"
      },
      {
        "synchronise": [
          null,
          null,
          "PetFeederShield_off",
          "PetFeederShield_off",
          null,
          null,
          null,
          null
        ],
        "result": "PetFeederShield_off"
      },
      {
        "synchronise": [
          null,
          null,
          "PetFeederShield_on",
          "PetFeederShield_on",
          null,
          null,
          null,
          null
        ],
        "result": "PetFeederShield_on"
      },
      {
        "synchronise": [
          null,
          null,
          "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          null,
          null,
          null,
          "PetFeederShield_PetFeederShield_1_FeedMyPet0_0",
          "PetFeederShield_PetFeederShield_1_FeedMyPet0_0"
        ],
        "result": "PetFeederShield_PetFeederShield_1_FeedMyPet0_0"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          "switch_switch_1_BigTurnOFF0_0",
          "switch_switch_1_BigTurnOFF0_0",
          null,
          null,
          "switch_switch_1_BigTurnOFF0_0"
        ],
        "result": "switch_switch_1_BigTurnOFF0_0"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          "switch_switch_1_BigTurnOFF1_0",
          null,
          "switch_switch_1_BigTurnOFF1_0",
          null,
          "switch_switch_1_BigTurnOFF1_0"
        ],
        "result": "switch_switch_1_BigTurnOFF1_0"
      }
    ]
  }
}