{
  "jani-version": 1,
  "name": "Security/KSA22/KSA22_2.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "carbonDioxide_Env_Evt"
    },
    {
      "name": "carbonDioxideMeasurement_carbonDioxide_Evt_1"
    },
    {
      "name": "power_Env_Evt"
    },
    {
      "name": "powerMeter_power_Evt_1"
    },
    {
      "name": "switch_switch_1_CO2Vent0_0"
    },
    {
      "name": "switch_switch_1_CO2Vent0_1"
    },
    {
      "name": "switch_switch_1_EnergySaver0_0"
    }
  ],
  "variables": [
    {
      "name": "carbonDioxideMeasurement_carbonDioxide_1_env_clk",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "timer_switch_switch_1",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "carbonDioxide_Env",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "step",
      "type": "real",
      "initial-value": 5
    },
    {
      "name": "power_Env",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "carbonDioxideMeasurement_carbonDioxide_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "state_active_20",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "switch_switch_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "powerMeter_power_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "local_switch_switch_1",
      "type": "real",
      "initial-value": 0
    },
    {
      "name": "delta",
      "type": "real",
      "initial-value": 60
    },
    {
      "name": "level_20",
      "type": "real"
    },
    {
      "name": "threshold_21",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "carbonDioxideMeasurement_carbonDioxide_Dev_1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "carbonDioxide_Env_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "carbonDioxideMeasurement_carbonDioxide_1",
              "right": "carbonDioxide_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "carbonDioxideMeasurement_carbonDioxide_Evt_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "carbonDioxideMeasurement_carbonDioxide_1",
              "right": "carbonDioxide_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "carbonDioxideMeasurement_carbonDioxide_1",
                  "value": "carbonDioxide_Env"
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "carbonDioxideMeasurement_carbonDioxide_Evt_1",
          "guard": {
            "exp": {
              "op": "<",
              "left": "carbonDioxideMeasurement_carbonDioxide_1",
              "right": "carbonDioxide_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "carbonDioxideMeasurement_carbonDioxide_1",
                  "value": "carbonDioxide_Env"
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "carbonDioxide_Env_Model",
      "locations": [
        {
          "name": "mode0"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "carbonDioxide_Env_Evt",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "≥",
                "left": "carbonDioxide_Env",
                "right": "step"
              },
              "right": {
                "op": "≥",
                "left": "carbonDioxideMeasurement_carbonDioxide_1_env_clk",
                "right": 0
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "carbonDioxide_Env",
                  "value": {
                    "op": "-",
                    "left": "carbonDioxide_Env",
                    "right": "step"
                  }
                },
                {
                  "ref": "carbonDioxideMeasurement_carbonDioxide_1_env_clk",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "carbonDioxide_Env_Evt",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "<",
                "left": "carbonDioxide_Env",
                "right": {
                  "op": "-",
                  "left": 100,
                  "right": "step"
                }
              },
              "right": {
                "op": "≥",
                "left": "carbonDioxideMeasurement_carbonDioxide_1_env_clk",
                "right": 0
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "carbonDioxide_Env",
                  "value": {
                    "op": "+",
                    "left": "carbonDioxide_Env",
                    "right": "step"
                  }
                },
                {
                  "ref": "carbonDioxideMeasurement_carbonDioxide_1_env_clk",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "powerMeter_power_Dev_1",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "power_Env_Evt",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "powerMeter_power_1",
              "right": "power_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "powerMeter_power_Evt_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "powerMeter_power_1",
              "right": "power_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "powerMeter_power_1",
                  "value": "power_Env"
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "powerMeter_power_Evt_1",
          "guard": {
            "exp": {
              "op": "<",
              "left": "powerMeter_power_1",
              "right": "power_Env"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "powerMeter_power_1",
                  "value": "power_Env"
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "power_Env_Model",
      "locations": [
        {
          "name": "mode0"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "power_Env_Evt",
          "guard": {
            "exp": {
              "op": "<",
              "left": "power_Env",
              "right": {
                "op": "-",
                "left": 100,
                "right": "step"
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "power_Env",
                  "value": {
                    "op": "+",
                    "left": "power_Env",
                    "right": "step"
                  }
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "CO2Vent0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "mode3"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "carbonDioxideMeasurement_carbonDioxide_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_CO2Vent0_0",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "state_active_20",
                "right": 0
              },
              "right": {
                "op": ">",
                "left": "carbonDioxideMeasurement_carbonDioxide_1",
                "right": "level_20"
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 97
                },
                {
                  "ref": "state_active_20",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_3",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "level_20",
              "right": "carbonDioxideMeasurement_carbonDioxide_1"
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_4",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "state_active_20",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode3"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "switch_switch_1_CO2Vent0_1",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "≥",
                "left": "state_active_20",
                "right": 0
              },
              "right": {
                "op": "≥",
                "left": "level_20",
                "right": "carbonDioxideMeasurement_carbonDioxide_1"
              }
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "state_active_20",
                  "value": 0
                },
                {
                  "ref": "switch_switch_1",
                  "value": 96
                }
              ]
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_5",
          "guard": {
            "exp": {
              "op": ">",
              "left": "carbonDioxideMeasurement_carbonDioxide_1",
              "right": "level_20"
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        },
        {
          "location": "mode3",
          "action": "nosync_6",
          "guard": {
            "exp": {
              "op": "≤",
              "left": "state_active_20",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "EnergySaver0",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "powerMeter_power_Evt_1",
          "destinations": [
            {
              "location": "mode1"
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_EnergySaver0_0",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "powerMeter_power_1",
              "right": "threshold_21"
            }
          },
          "destinations": [
            {
              "location": "mode0",
              "assignments": [
                {
                  "ref": "switch_switch_1",
                  "value": 96
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "nosync_7",
          "guard": {
            "exp": {
              "op": ">",
              "left": "threshold_21",
              "right": "powerMeter_power_1"
            }
          },
          "destinations": [
            {
              "location": "mode0"
            }
          ]
        }
      ]
    },
    {
      "name": "switch_switch_1_attr",
      "locations": [
        {
          "name": "mode0"
        },
        {
          "name": "mode1"
        },
        {
          "name": "mode2"
        },
        {
          "name": "conflict"
        }
      ],
      "initial-locations": [
        "mode0"
      ],
      "edges": [
        {
          "location": "mode0",
          "action": "switch_switch_1_CO2Vent0_0",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_CO2Vent0_1",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode0",
          "action": "switch_switch_1_EnergySaver0_0",
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_CO2Vent0_0",
          "destinations": [
            {
              "location": "mode2",
              "assignments": [
                {
                  "ref": "local_switch_switch_1",
                  "value": "switch_switch_1"
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_CO2Vent0_1",
          "destinations": [
            {
              "location": "mode2",
              "assignments": [
                {
                  "ref": "local_switch_switch_1",
                  "value": "switch_switch_1"
                }
              ]
            }
          ]
        },
        {
          "location": "mode1",
          "action": "switch_switch_1_EnergySaver0_0",
          "destinations": [
            {
              "location": "mode2",
              "assignments": [
                {
                  "ref": "local_switch_switch_1",
                  "value": "switch_switch_1"
                }
              ]
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_8",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "≥",
                "left": "local_switch_switch_1",
                "right": "switch_switch_1"
              },
              "right": {
                "op": ">",
                "left": "delta",
                "right": "timer_switch_switch_1"
              }
            }
          },
          "destinations": [
            {
              "location": "conflict"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_9",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "<",
                "left": "local_switch_switch_1",
                "right": "switch_switch_1"
              },
              "right": {
                "op": ">",
                "left": "delta",
                "right": "timer_switch_switch_1"
              }
            }
          },
          "destinations": [
            {
              "location": "conflict"
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_10",
          "guard": {
            "exp": {
              "op": ">",
              "left": "timer_switch_switch_1",
              "right": "delta"
            }
          },
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "mode2",
          "action": "nosync_11",
          "guard": {
            "exp": {
              "op": "=",
              "left": "local_switch_switch_1",
              "right": "switch_switch_1"
            }
          },
          "destinations": [
            {
              "location": "mode1",
              "assignments": [
                {
                  "ref": "timer_switch_switch_1",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "carbonDioxideMeasurement_carbonDioxide_Dev_1"
      },
      {
        "automaton": "carbonDioxide_Env_Model"
      },
      {
        "automaton": "powerMeter_power_Dev_1"
      },
      {
        "automaton": "power_Env_Model"
      },
      {
        "automaton": "CO2Vent0"
      },
      {
        "automaton": "EnergySaver0"
      },
      {
        "automaton": "switch_switch_1_attr"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "carbonDioxide_Env_Evt",
          "carbonDioxide_Env_Evt",
          null,
          null,
          null,
          null,
          null
        ],
        "result": "carbonDioxide_Env_Evt"
      },
      {
        "synchronise": [
          "carbonDioxideMeasurement_carbonDioxide_Evt_1",
          null,
          null,
          null,
          "carbonDioxideMeasurement_carbonDioxide_Evt_1",
          null,
          null
        ],
        "result": "carbonDioxideMeasurement_carbonDioxide_Evt_1"
      },
      {
        "synchronise": [
          null,
          null,
          "power_Env_Evt",
          "power_Env_Evt",
          null,
          null,
          null
        ],
        "result": "power_Env_Evt"
      },
      {
        "synchronise": [
          null,
          null,
          "powerMeter_power_Evt_1",
          null,
          null,
          "powerMeter_power_Evt_1",
          null
        ],
        "result": "powerMeter_power_Evt_1"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          "switch_switch_1_CO2Vent0_0",
          null,
          "switch_switch_1_CO2Vent0_0"
        ],
        "result": "switch_switch_1_CO2Vent0_0"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          "switch_switch_1_CO2Vent0_1",
          null,
          "switch_switch_1_CO2Vent0_1"
        ],
        "result": "switch_switch_1_CO2Vent0_1"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          null,
          "switch_switch_1_EnergySaver0_0",
          "switch_switch_1_EnergySaver0_0"
        ],
        "result": "switch_switch_1_EnergySaver0_0"
      }
    ]
  }
}