{
  "jani-version": 1,
  "name": "Jobshop/jobshop_2_4.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "b1"
    },
    {
      "name": "FIN1"
    },
    {
      "name": "b2"
    },
    {
      "name": "FIN2"
    }
  ],
  "variables": [
    {
      "name": "x1",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "x2",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "m1",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "m2",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "m3",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "m4",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "d11",
      "type": "real"
    },
    {
      "name": "d12",
      "type": "real"
    },
    {
      "name": "d13",
      "type": "real"
    },
    {
      "name": "d14",
      "type": "real"
    },
    {
      "name": "d21",
      "type": "real"
    },
    {
      "name": "d22",
      "type": "real"
    },
    {
      "name": "d23",
      "type": "real"
    },
    {
      "name": "d24",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "job1",
      "locations": [
        {
          "name": "I1"
        },
        {
          "name": "J1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d13",
              "right": "x1"
            }
          }
        },
        {
          "name": "K1"
        },
        {
          "name": "L1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d11",
              "right": "x1"
            }
          }
        },
        {
          "name": "M1"
        },
        {
          "name": "N1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d12",
              "right": "x1"
            }
          }
        },
        {
          "name": "P1"
        },
        {
          "name": "Q1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d14",
              "right": "x1"
            }
          }
        },
        {
          "name": "End1"
        }
      ],
      "initial_locations": [
        "I1"
      ],
      "edges": [
        {
          "location": "I1",
          "guard": {
            "op": "=",
            "left": "m3",
            "right": 0
          },
          "destinations": [
            {
              "location": "J1",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "m3",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "J1",
          "guard": {
            "op": "=",
            "left": "d13",
            "right": "x1"
          },
          "destinations": [
            {
              "location": "K1",
              "assignments": [
                {
                  "ref": "m3",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "K1",
          "guard": {
            "op": "=",
            "left": "m1",
            "right": 0
          },
          "destinations": [
            {
              "location": "L1",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "m1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "L1",
          "guard": {
            "op": "=",
            "left": "d11",
            "right": "x1"
          },
          "destinations": [
            {
              "location": "M1",
              "assignments": [
                {
                  "ref": "m1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "M1",
          "guard": {
            "op": "=",
            "left": "m2",
            "right": 0
          },
          "destinations": [
            {
              "location": "N1",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "m2",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "N1",
          "guard": {
            "op": "=",
            "left": "d12",
            "right": "x1"
          },
          "destinations": [
            {
              "location": "P1",
              "assignments": [
                {
                  "ref": "m3",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "P1",
          "guard": {
            "op": "=",
            "left": "m4",
            "right": 0
          },
          "destinations": [
            {
              "location": "Q1",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "m4",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "Q1",
          "guard": {
            "op": "=",
            "left": "d14",
            "right": "x1"
          },
          "destinations": [
            {
              "location": "End1",
              "assignments": [
                {
                  "ref": "m4",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "job2",
      "locations": [
        {
          "name": "I2"
        },
        {
          "name": "J2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d22",
              "right": "x2"
            }
          }
        },
        {
          "name": "K2"
        },
        {
          "name": "L2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d23",
              "right": "x2"
            }
          }
        },
        {
          "name": "M2"
        },
        {
          "name": "N2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d21",
              "right": "x2"
            }
          }
        },
        {
          "name": "P2"
        },
        {
          "name": "Q2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "d24",
              "right": "x2"
            }
          }
        },
        {
          "name": "End2"
        }
      ],
      "initial_locations": [
        "I2"
      ],
      "edges": [
        {
          "location": "I2",
          "guard": {
            "op": "=",
            "left": "m2",
            "right": 0
          },
          "destinations": [
            {
              "location": "J2",
              "assignments": [
                {
                  "ref": "x2",
                  "value": 0
                },
                {
                  "ref": "m2",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "J2",
          "guard": {
            "op": "=",
            "left": "d22",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "K2",
              "assignments": [
                {
                  "ref": "m2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "K2",
          "guard": {
            "op": "=",
            "left": "m3",
            "right": 0
          },
          "destinations": [
            {
              "location": "L2",
              "assignments": [
                {
                  "ref": "x2",
                  "value": 0
                },
                {
                  "ref": "m3",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "L2",
          "guard": {
            "op": "=",
            "left": "d23",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "M2",
              "assignments": [
                {
                  "ref": "m3",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "M2",
          "guard": {
            "op": "=",
            "left": "m1",
            "right": 0
          },
          "destinations": [
            {
              "location": "N2",
              "assignments": [
                {
                  "ref": "x2",
                  "value": 0
                },
                {
                  "ref": "m1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "N2",
          "guard": {
            "op": "=",
            "left": "d21",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "P2",
              "assignments": [
                {
                  "ref": "m1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "P2",
          "guard": {
            "op": "=",
            "left": "m4",
            "right": 0
          },
          "destinations": [
            {
              "location": "Q2",
              "assignments": [
                {
                  "ref": "x2",
                  "value": 0
                },
                {
                  "ref": "m4",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "Q2",
          "guard": {
            "op": "=",
            "left": "d24",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "End2",
              "assignments": [
                {
                  "ref": "m4",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "job1"
      },
      {
        "automaton": "job2"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "b1",
          null
        ],
        "result": "b1"
      },
      {
        "synchronise": [
          "FIN1",
          null
        ],
        "result": "FIN1"
      },
      {
        "synchronise": [
          null,
          "b2"
        ],
        "result": "b2"
      },
      {
        "synchronise": [
          null,
          "FIN2"
        ],
        "result": "FIN2"
      }
    ]
  }
}