{
  "jani-version": 1,
  "name": "Packaging/packaging.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "fillm"
    },
    {
      "name": "shipm"
    },
    {
      "name": "resumem"
    },
    {
      "name": "errpm"
    },
    {
      "name": "packm"
    },
    {
      "name": "resolvem"
    }
  ],
  "variables": [
    {
      "name": "x",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "y",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "a",
      "type": "real"
    },
    {
      "name": "b",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "FFS",
      "locations": [
        {
          "name": "f0"
        },
        {
          "name": "f1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 2,
              "right": "x"
            }
          }
        },
        {
          "name": "f2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "b",
              "right": "x"
            }
          }
        }
      ],
      "initial_locations": [
        "f0"
      ],
      "edges": [
        {
          "location": "f0",
          "destinations": [
            {
              "location": "f1",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "f1",
          "destinations": [
            {
              "location": "f2",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "f1",
          "guard": {
            "op": ">",
            "left": 1,
            "right": "x"
          },
          "destinations": [
            {
              "location": "f0",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "f2",
          "guard": {
            "op": ">",
            "left": "x",
            "right": "a"
          },
          "destinations": [
            {
              "location": "f1",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "Monitor",
      "locations": [
        {
          "name": "m0"
        },
        {
          "name": "m1"
        },
        {
          "name": "m2"
        },
        {
          "name": "m3"
        },
        {
          "name": "risk"
        }
      ],
      "initial_locations": [
        "m0"
      ],
      "edges": [
        {
          "location": "m0",
          "destinations": [
            {
              "location": "m1"
            }
          ]
        },
        {
          "location": "m0",
          "destinations": [
            {
              "location": "m0"
            }
          ]
        },
        {
          "location": "m1",
          "destinations": [
            {
              "location": "m2"
            }
          ]
        },
        {
          "location": "m1",
          "destinations": [
            {
              "location": "m1"
            }
          ]
        },
        {
          "location": "m1",
          "destinations": [
            {
              "location": "m0"
            }
          ]
        },
        {
          "location": "m2",
          "destinations": [
            {
              "location": "m3"
            }
          ]
        },
        {
          "location": "m2",
          "destinations": [
            {
              "location": "m1"
            }
          ]
        },
        {
          "location": "m3",
          "destinations": [
            {
              "location": "m1"
            }
          ]
        },
        {
          "location": "m3",
          "destinations": [
            {
              "location": "risk"
            }
          ]
        }
      ]
    },
    {
      "name": "Packaging",
      "locations": [
        {
          "name": "p0",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 5,
              "right": "y"
            }
          }
        },
        {
          "name": "p1",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 50,
              "right": "y"
            }
          }
        }
      ],
      "initial_locations": [
        "p0"
      ],
      "edges": [
        {
          "location": "p0",
          "destinations": [
            {
              "location": "p0",
              "assignments": [
                {
                  "ref": "y",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "p0",
          "destinations": [
            {
              "location": "p1",
              "assignments": [
                {
                  "ref": "y",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "p1",
          "guard": {
            "op": ">",
            "left": "y",
            "right": 10
          },
          "destinations": [
            {
              "location": "p0",
              "assignments": [
                {
                  "ref": "y",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "FFS"
      },
      {
        "automaton": "Monitor"
      },
      {
        "automaton": "Packaging"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "fillm",
          "fillm",
          null
        ],
        "result": "fillm"
      },
      {
        "synchronise": [
          "shipm",
          "shipm",
          null
        ],
        "result": "shipm"
      },
      {
        "synchronise": [
          "resumem",
          "resumem",
          null
        ],
        "result": "resumem"
      },
      {
        "synchronise": [
          "errpm",
          "errpm",
          "errpm"
        ],
        "result": "errpm"
      },
      {
        "synchronise": [
          null,
          "packm",
          "packm"
        ],
        "result": "packm"
      },
      {
        "synchronise": [
          null,
          "resolvem",
          "resolvem"
        ],
        "result": "resolvem"
      }
    ]
  }
}