{
  "jani-version": 1,
  "name": "Scheduling/Thales_FMTV_Challenge/FMTV/FMTV1/FMTV_1_A3.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "start"
    },
    {
      "name": "T2done"
    },
    {
      "name": "init_buffer_0"
    },
    {
      "name": "init_buffer_1"
    },
    {
      "name": "init_buffer_2"
    },
    {
      "name": "init_buffer_3"
    },
    {
      "name": "T3_done"
    },
    {
      "name": "T3_start"
    },
    {
      "name": "T4_start_empty"
    },
    {
      "name": "T4_start_nonempty"
    },
    {
      "name": "T4_done_empty"
    },
    {
      "name": "T4_done_nonempty"
    }
  ],
  "variables": [
    {
      "name": "ckT1T2",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "ckT3",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "ckT4",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "frame_in_3",
      "type": "real",
      "initial_value": 2
    },
    {
      "name": "frame_in_4",
      "type": "real",
      "initial_value": 1
    },
    {
      "name": "register23",
      "type": "real",
      "initial_value": 3
    },
    {
      "name": "buffer34_1",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "buffer34_2",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "buffer34_3",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "buffer34_highest",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "e2e",
      "type": "real"
    },
    {
      "name": "P3_uncertain",
      "type": "real"
    },
    {
      "name": "P4_uncertain",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "cameraT1T2",
      "locations": [
        {
          "name": "camera0",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT1T2",
              "right": 0
            }
          }
        },
        {
          "name": "camera1",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT1T2",
              "right": 0
            }
          }
        },
        {
          "name": "camera2",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT1T2",
              "right": 0
            }
          }
        },
        {
          "name": "camera3",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT1T2",
              "right": 0
            }
          }
        },
        {
          "name": "camera4",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT1T2",
              "right": 0
            }
          }
        },
        {
          "name": "T1T2",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 19,
              "right": "ckT1T2"
            }
          }
        },
        {
          "name": "T1T2done"
        }
      ],
      "initial_locations": [
        "camera0"
      ],
      "edges": [
        {
          "location": "camera0",
          "destinations": [
            {
              "location": "camera1",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": 0
                },
                {
                  "ref": "buffer34_highest",
                  "value": 0
                },
                {
                  "ref": "buffer34_3",
                  "value": 0
                },
                {
                  "ref": "buffer34_2",
                  "value": 0
                },
                {
                  "ref": "buffer34_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "camera0",
          "destinations": [
            {
              "location": "camera1",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_3",
                  "value": 0
                },
                {
                  "ref": "buffer34_2",
                  "value": 0
                },
                {
                  "ref": "buffer34_1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "camera0",
          "destinations": [
            {
              "location": "camera1",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_3",
                  "value": 0
                },
                {
                  "ref": "buffer34_2",
                  "value": 1
                },
                {
                  "ref": "buffer34_1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "camera0",
          "destinations": [
            {
              "location": "camera1",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_highest",
                  "value": 1
                },
                {
                  "ref": "buffer34_3",
                  "value": 1
                },
                {
                  "ref": "buffer34_2",
                  "value": 1
                },
                {
                  "ref": "buffer34_1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "camera1",
          "destinations": [
            {
              "location": "camera2",
              "assignments": [
                {
                  "ref": "frame_in_4",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "camera1",
          "destinations": [
            {
              "location": "camera2",
              "assignments": [
                {
                  "ref": "frame_in_4",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "camera2",
          "destinations": [
            {
              "location": "camera3",
              "assignments": [
                {
                  "ref": "register23",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "camera2",
          "destinations": [
            {
              "location": "camera3"
            }
          ]
        },
        {
          "location": "camera3",
          "destinations": [
            {
              "location": "camera4",
              "assignments": [
                {
                  "ref": "frame_in_3",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "camera3",
          "destinations": [
            {
              "location": "camera4"
            }
          ]
        },
        {
          "location": "camera4",
          "destinations": [
            {
              "location": "T1T2"
            }
          ]
        },
        {
          "location": "T1T2",
          "guard": {
            "op": ">",
            "left": "ckT1T2",
            "right": 17
          },
          "destinations": [
            {
              "location": "T1T2done",
              "assignments": [
                {
                  "ref": "register23",
                  "value": 200
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "T3",
      "locations": [
        {
          "name": "T3preinit"
        },
        {
          "name": "T3process",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 8,
              "right": "ckT3"
            }
          }
        },
        {
          "name": "T3wait",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "P3_uncertain",
              "right": "ckT3"
            }
          }
        }
      ],
      "initial_locations": [
        "T3preinit"
      ],
      "edges": [
        {
          "location": "T3preinit",
          "destinations": [
            {
              "location": "T3wait"
            }
          ]
        },
        {
          "location": "T3preinit",
          "guard": {
            "op": ">",
            "left": 8,
            "right": "ckT3"
          },
          "destinations": [
            {
              "location": "T3process"
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_3",
              "right": 0
            },
            "right": {
              "op": "=",
              "left": "ckT3",
              "right": 8
            }
          },
          "destinations": [
            {
              "location": "T3wait"
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_2",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer34_3",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": ">",
                  "left": "buffer34_highest",
                  "right": "frame_in_3"
                },
                "right": {
                  "op": "=",
                  "left": "ckT3",
                  "right": 8
                }
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait"
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_2",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer34_3",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "<",
                  "left": "buffer34_highest",
                  "right": "frame_in_3"
                },
                "right": {
                  "op": "=",
                  "left": "ckT3",
                  "right": 8
                }
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": "frame_in_3"
                },
                {
                  "ref": "buffer34_3",
                  "value": "frame_in_3"
                }
              ]
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer34_2",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": ">",
                  "left": "buffer34_highest",
                  "right": "frame_in_3"
                },
                "right": {
                  "op": "=",
                  "left": "ckT3",
                  "right": 8
                }
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait"
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer34_2",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "<",
                  "left": "buffer34_highest",
                  "right": "frame_in_3"
                },
                "right": {
                  "op": "=",
                  "left": "ckT3",
                  "right": 8
                }
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": "frame_in_3"
                },
                {
                  "ref": "buffer34_2",
                  "value": "frame_in_3"
                }
              ]
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "buffer34_highest",
                "right": "frame_in_3"
              },
              "right": {
                "op": "=",
                "left": "ckT3",
                "right": 8
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait"
            }
          ]
        },
        {
          "location": "T3process",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "<",
                "left": "buffer34_highest",
                "right": "frame_in_3"
              },
              "right": {
                "op": "=",
                "left": "ckT3",
                "right": 8
              }
            }
          },
          "destinations": [
            {
              "location": "T3wait",
              "assignments": [
                {
                  "ref": "buffer34_highest",
                  "value": "frame_in_3"
                },
                {
                  "ref": "buffer34_1",
                  "value": "frame_in_3"
                }
              ]
            }
          ]
        },
        {
          "location": "T3wait",
          "guard": {
            "op": "=",
            "left": "P3_uncertain",
            "right": "ckT3"
          },
          "destinations": [
            {
              "location": "T3process",
              "assignments": [
                {
                  "ref": "ckT3",
                  "value": 0
                },
                {
                  "ref": "frame_in_3",
                  "value": "register23"
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "T4",
      "locations": [
        {
          "name": "T4preinit"
        },
        {
          "name": "T4process_nonempty",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "ckT4"
            }
          }
        },
        {
          "name": "T4process_empty",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 1,
              "right": "ckT4"
            }
          }
        },
        {
          "name": "T4wait",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "P4_uncertain",
              "right": "ckT4"
            }
          }
        },
        {
          "name": "T4end_ok",
          "time-progress": {
            "exp": {
              "op": "=",
              "left": "ckT4",
              "right": 0
            }
          }
        }
      ],
      "initial_locations": [
        "T4preinit"
      ],
      "edges": [
        {
          "location": "T4preinit",
          "destinations": [
            {
              "location": "T4wait"
            }
          ]
        },
        {
          "location": "T4process_nonempty",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "frame_in_4",
              "right": 200
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "ckT4",
                "right": 10
              },
              "right": {
                "op": "=",
                "left": "e2e",
                "right": {
                  "op": "+",
                  "left": 28,
                  "right": "ckT1T2"
                }
              }
            }
          },
          "destinations": [
            {
              "location": "T4end_ok",
              "assignments": [
                {
                  "ref": "ckT4",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "T4process_nonempty",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<",
              "left": "frame_in_4",
              "right": 200
            },
            "right": {
              "op": "=",
              "left": "ckT4",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "T4wait"
            }
          ]
        },
        {
          "location": "T4process_empty",
          "guard": {
            "op": "=",
            "left": "ckT4",
            "right": 1
          },
          "destinations": [
            {
              "location": "T4wait"
            }
          ]
        },
        {
          "location": "T4wait",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "=",
              "left": "P4_uncertain",
              "right": "ckT4"
            }
          },
          "destinations": [
            {
              "location": "T4process_empty",
              "assignments": [
                {
                  "ref": "ckT4",
                  "value": 0
                },
                {
                  "ref": "frame_in_4",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "T4wait",
          "guard": {
            "op": "∧",
            "left": {
              "op": "≥",
              "left": "buffer34_1",
              "right": 0
            },
            "right": {
              "op": "=",
              "left": "P4_uncertain",
              "right": "ckT4"
            }
          },
          "destinations": [
            {
              "location": "T4process_nonempty",
              "assignments": [
                {
                  "ref": "ckT4",
                  "value": 0
                },
                {
                  "ref": "buffer34_1",
                  "value": "buffer34_2"
                },
                {
                  "ref": "buffer34_2",
                  "value": "buffer34_3"
                },
                {
                  "ref": "buffer34_3",
                  "value": 0
                },
                {
                  "ref": "frame_in_4",
                  "value": "buffer34_1"
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "cameraT1T2"
      },
      {
        "automaton": "T3"
      },
      {
        "automaton": "T4"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "start",
          "start",
          "start"
        ],
        "result": "start"
      },
      {
        "synchronise": [
          "T2done",
          null,
          null
        ],
        "result": "T2done"
      },
      {
        "synchronise": [
          "init_buffer_0",
          null,
          null
        ],
        "result": "init_buffer_0"
      },
      {
        "synchronise": [
          "init_buffer_1",
          null,
          null
        ],
        "result": "init_buffer_1"
      },
      {
        "synchronise": [
          "init_buffer_2",
          null,
          null
        ],
        "result": "init_buffer_2"
      },
      {
        "synchronise": [
          "init_buffer_3",
          null,
          null
        ],
        "result": "init_buffer_3"
      },
      {
        "synchronise": [
          null,
          "T3_done",
          null
        ],
        "result": "T3_done"
      },
      {
        "synchronise": [
          null,
          "T3_start",
          null
        ],
        "result": "T3_start"
      },
      {
        "synchronise": [
          null,
          null,
          "T4_start_empty"
        ],
        "result": "T4_start_empty"
      },
      {
        "synchronise": [
          null,
          null,
          "T4_start_nonempty"
        ],
        "result": "T4_start_nonempty"
      },
      {
        "synchronise": [
          null,
          null,
          "T4_done_empty"
        ],
        "result": "T4_done_empty"
      },
      {
        "synchronise": [
          null,
          null,
          "T4_done_nonempty"
        ],
        "result": "T4_done_nonempty"
      }
    ]
  }
}