{
  "jani-version": 1,
  "name": "Fischer/FischerHRSV02/fischerHRSV02_2.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [],
  "variables": [
    {
      "name": "x_1",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "x_2",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "lock",
      "type": "int",
      "initial_value": 0
    },
    {
      "name": "min_rw",
      "type": "real"
    },
    {
      "name": "max_rw",
      "type": "real"
    },
    {
      "name": "min_delay",
      "type": "real"
    },
    {
      "name": "max_delay",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "process_1",
      "locations": [
        {
          "name": "start_1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_rw",
              "right": "x_1"
            }
          }
        },
        {
          "name": "set_1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_rw",
              "right": "x_1"
            }
          }
        },
        {
          "name": "tryenter_1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_delay",
              "right": "x_1"
            }
          }
        },
        {
          "name": "cs_1"
        }
      ],
      "initial_locations": [
        "start_1"
      ],
      "edges": [
        {
          "location": "start_1",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<>",
              "left": "lock",
              "right": 0
            },
            "right": {
              "op": "≥",
              "left": "x_1",
              "right": "min_rw"
            }
          },
          "destinations": [
            {
              "location": "start_1",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "start_1",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "lock",
              "right": 0
            },
            "right": {
              "op": "≥",
              "left": "x_1",
              "right": "min_rw"
            }
          },
          "destinations": [
            {
              "location": "set_1",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "set_1",
          "guard": {
            "op": "≥",
            "left": "x_1",
            "right": "min_rw"
          },
          "destinations": [
            {
              "location": "tryenter_1",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "lock",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "tryenter_1",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "lock",
              "right": 1
            },
            "right": {
              "op": "≥",
              "left": "x_1",
              "right": "min_delay"
            }
          },
          "destinations": [
            {
              "location": "cs_1"
            }
          ]
        },
        {
          "location": "tryenter_1",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<>",
              "left": "lock",
              "right": 1
            },
            "right": {
              "op": "≥",
              "left": "x_1",
              "right": "min_delay"
            }
          },
          "destinations": [
            {
              "location": "start_1",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "cs_1",
          "destinations": [
            {
              "location": "start_1",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "lock",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "process_2",
      "locations": [
        {
          "name": "start_2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_rw",
              "right": "x_2"
            }
          }
        },
        {
          "name": "set_2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_rw",
              "right": "x_2"
            }
          }
        },
        {
          "name": "tryenter_2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "max_delay",
              "right": "x_2"
            }
          }
        },
        {
          "name": "cs_2"
        }
      ],
      "initial_locations": [
        "start_2"
      ],
      "edges": [
        {
          "location": "start_2",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<>",
              "left": "lock",
              "right": 0
            },
            "right": {
              "op": "≥",
              "left": "x_2",
              "right": "min_rw"
            }
          },
          "destinations": [
            {
              "location": "start_2",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "start_2",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "lock",
              "right": 0
            },
            "right": {
              "op": "≥",
              "left": "x_2",
              "right": "min_rw"
            }
          },
          "destinations": [
            {
              "location": "set_2",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "set_2",
          "guard": {
            "op": "≥",
            "left": "x_2",
            "right": "min_rw"
          },
          "destinations": [
            {
              "location": "tryenter_2",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "lock",
                  "value": 2
                }
              ]
            }
          ]
        },
        {
          "location": "tryenter_2",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "lock",
              "right": 2
            },
            "right": {
              "op": "≥",
              "left": "x_2",
              "right": "min_delay"
            }
          },
          "destinations": [
            {
              "location": "cs_2"
            }
          ]
        },
        {
          "location": "tryenter_2",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<>",
              "left": "lock",
              "right": 2
            },
            "right": {
              "op": "≥",
              "left": "x_2",
              "right": "min_delay"
            }
          },
          "destinations": [
            {
              "location": "start_2",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "cs_2",
          "destinations": [
            {
              "location": "start_2",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "lock",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "process_1"
      },
      {
        "automaton": "process_2"
      }
    ],
    "syncs": []
  }
}