{
  "jani-version": 1,
  "name": "BRP/BRPAAPP21/BRPAAPP21_GFSinRC.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "S_in"
    },
    {
      "name": "sndD"
    },
    {
      "name": "rcvA"
    },
    {
      "name": "S_DK"
    },
    {
      "name": "S_NOK"
    },
    {
      "name": "S_OK"
    },
    {
      "name": "rcvD"
    },
    {
      "name": "sndA"
    },
    {
      "name": "R_NOK"
    },
    {
      "name": "R_OK"
    },
    {
      "name": "R_FST"
    },
    {
      "name": "R_INC"
    },
    {
      "name": "lostK"
    },
    {
      "name": "lostL"
    }
  ],
  "variables": [
    {
      "name": "x",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "z",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "u",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "v",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "i",
      "type": "real",
      "initial_value": 1
    },
    {
      "name": "rc",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "b1",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "bN",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "rb1",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "rbN",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "ab",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "rab",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "exp_ab",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "SYNC",
      "type": "real"
    },
    {
      "name": "TS",
      "type": "real"
    },
    {
      "name": "TR",
      "type": "real"
    },
    {
      "name": "TD",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "monitor",
      "locations": [
        {
          "name": "s0"
        },
        {
          "name": "s1"
        }
      ],
      "initial_locations": [
        "s0"
      ],
      "edges": [
        {
          "location": "s0",
          "destinations": [
            {
              "location": "s1"
            }
          ]
        },
        {
          "location": "s0",
          "destinations": [
            {
              "location": "s0"
            }
          ]
        },
        {
          "location": "s0",
          "destinations": [
            {
              "location": "s0"
            }
          ]
        },
        {
          "location": "s1",
          "destinations": [
            {
              "location": "s1"
            }
          ]
        }
      ]
    },
    {
      "name": "sender",
      "locations": [
        {
          "name": "idleS",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "x",
              "right": 0
            }
          }
        },
        {
          "name": "next_frame"
        },
        {
          "name": "wait_ack",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "TS",
              "right": "x"
            }
          }
        },
        {
          "name": "success"
        },
        {
          "name": "error",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "SYNC",
              "right": "x"
            }
          }
        }
      ],
      "initial_locations": [
        "idleS"
      ],
      "edges": [
        {
          "location": "idleS",
          "destinations": [
            {
              "location": "next_frame",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "b1",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "next_frame",
          "guard": {
            "op": "<",
            "left": "i",
            "right": 2
          },
          "destinations": [
            {
              "location": "wait_ack",
              "assignments": [
                {
                  "ref": "bN",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "next_frame",
          "guard": {
            "op": "=",
            "left": "i",
            "right": 2
          },
          "destinations": [
            {
              "location": "wait_ack",
              "assignments": [
                {
                  "ref": "bN",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "wait_ack",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rc",
              "right": 2
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "i",
                "right": 2
              },
              "right": {
                "op": "=",
                "left": "TS",
                "right": "x"
              }
            }
          },
          "destinations": [
            {
              "location": "error",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "i",
                  "value": 1
                },
                {
                  "ref": "rc",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "wait_ack",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rc",
              "right": 2
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "<",
                "left": "i",
                "right": 2
              },
              "right": {
                "op": "=",
                "left": "TS",
                "right": "x"
              }
            }
          },
          "destinations": [
            {
              "location": "error",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "i",
                  "value": 1
                },
                {
                  "ref": "rc",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "wait_ack",
          "guard": {
            "op": "≥",
            "left": "TS",
            "right": "x"
          },
          "destinations": [
            {
              "location": "success",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "rc",
                  "value": 0
                },
                {
                  "ref": "ab",
                  "value": {
                    "op": "-",
                    "left": 1,
                    "right": "ab"
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "wait_ack",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<",
              "left": "rc",
              "right": 2
            },
            "right": {
              "op": "=",
              "left": "TS",
              "right": "x"
            }
          },
          "destinations": [
            {
              "location": "wait_ack",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "rc",
                  "value": {
                    "op": "+",
                    "left": "rc",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "success",
          "guard": {
            "op": "<",
            "left": "i",
            "right": 2
          },
          "destinations": [
            {
              "location": "next_frame",
              "assignments": [
                {
                  "ref": "b1",
                  "value": 0
                },
                {
                  "ref": "i",
                  "value": {
                    "op": "+",
                    "left": "i",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "success",
          "guard": {
            "op": "=",
            "left": "i",
            "right": 2
          },
          "destinations": [
            {
              "location": "idleS",
              "assignments": [
                {
                  "ref": "i",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "error",
          "guard": {
            "op": "=",
            "left": "SYNC",
            "right": "x"
          },
          "destinations": [
            {
              "location": "idleS",
              "assignments": [
                {
                  "ref": "ab",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "receiver",
      "locations": [
        {
          "name": "new_file"
        },
        {
          "name": "fst_safe"
        },
        {
          "name": "frame_received"
        },
        {
          "name": "frame_reported"
        },
        {
          "name": "idleR",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "TR",
              "right": "z"
            }
          }
        }
      ],
      "initial_locations": [
        "new_file"
      ],
      "edges": [
        {
          "location": "new_file",
          "destinations": [
            {
              "location": "fst_safe",
              "assignments": [
                {
                  "ref": "z",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "fst_safe",
          "guard": {
            "op": "=",
            "left": "rb1",
            "right": 1
          },
          "destinations": [
            {
              "location": "frame_received",
              "assignments": [
                {
                  "ref": "exp_ab",
                  "value": "rab"
                }
              ]
            }
          ]
        },
        {
          "location": "frame_received",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rab",
              "right": "exp_ab"
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "rb1",
                "right": 1
              },
              "right": {
                "op": "=",
                "left": "rbN",
                "right": 0
              }
            }
          },
          "destinations": [
            {
              "location": "frame_reported",
              "assignments": [
                {
                  "ref": "rab",
                  "value": 0
                },
                {
                  "ref": "rb1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "frame_received",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rab",
              "right": "exp_ab"
            },
            "right": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "rb1",
                "right": 0
              },
              "right": {
                "op": "=",
                "left": "rbN",
                "right": 0
              }
            }
          },
          "destinations": [
            {
              "location": "frame_reported",
              "assignments": [
                {
                  "ref": "rab",
                  "value": 0
                },
                {
                  "ref": "rb1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "frame_received",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rab",
              "right": "exp_ab"
            },
            "right": {
              "op": "=",
              "left": "rbN",
              "right": 1
            }
          },
          "destinations": [
            {
              "location": "frame_reported",
              "assignments": [
                {
                  "ref": "rab",
                  "value": 0
                },
                {
                  "ref": "rb1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "frame_received",
          "guard": {
            "op": "=",
            "left": "rab",
            "right": {
              "op": "-",
              "left": 1,
              "right": "exp_ab"
            }
          },
          "destinations": [
            {
              "location": "idleR",
              "assignments": [
                {
                  "ref": "rab",
                  "value": 0
                },
                {
                  "ref": "rb1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "frame_reported",
          "destinations": [
            {
              "location": "idleR",
              "assignments": [
                {
                  "ref": "z",
                  "value": 0
                },
                {
                  "ref": "exp_ab",
                  "value": {
                    "op": "-",
                    "left": 1,
                    "right": "exp_ab"
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "idleR",
          "guard": {
            "op": "≥",
            "left": "TR",
            "right": "z"
          },
          "destinations": [
            {
              "location": "frame_received"
            }
          ]
        },
        {
          "location": "idleR",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rbN",
              "right": 0
            },
            "right": {
              "op": "=",
              "left": "TR",
              "right": "z"
            }
          },
          "destinations": [
            {
              "location": "new_file",
              "assignments": [
                {
                  "ref": "exp_ab",
                  "value": 0
                },
                {
                  "ref": "rbN",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "idleR",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "rbN",
              "right": 1
            },
            "right": {
              "op": "=",
              "left": "TR",
              "right": "z"
            }
          },
          "destinations": [
            {
              "location": "new_file",
              "assignments": [
                {
                  "ref": "exp_ab",
                  "value": 0
                },
                {
                  "ref": "rbN",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "channelK",
      "locations": [
        {
          "name": "startK",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "u",
              "right": 0
            }
          }
        },
        {
          "name": "in_transitK",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "TD",
              "right": "u"
            }
          }
        }
      ],
      "initial_locations": [
        "startK"
      ],
      "edges": [
        {
          "location": "startK",
          "destinations": [
            {
              "location": "in_transitK",
              "assignments": [
                {
                  "ref": "u",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "in_transitK",
          "destinations": [
            {
              "location": "startK"
            }
          ]
        },
        {
          "location": "in_transitK",
          "destinations": [
            {
              "location": "startK",
              "assignments": [
                {
                  "ref": "rab",
                  "value": "ab"
                },
                {
                  "ref": "rbN",
                  "value": "bN"
                },
                {
                  "ref": "rb1",
                  "value": "b1"
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "channelL",
      "locations": [
        {
          "name": "startL",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "v",
              "right": 0
            }
          }
        },
        {
          "name": "in_transitL",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "TD",
              "right": "v"
            }
          }
        }
      ],
      "initial_locations": [
        "startL"
      ],
      "edges": [
        {
          "location": "startL",
          "destinations": [
            {
              "location": "in_transitL",
              "assignments": [
                {
                  "ref": "v",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "in_transitL",
          "destinations": [
            {
              "location": "startL"
            }
          ]
        },
        {
          "location": "in_transitL",
          "destinations": [
            {
              "location": "startL"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "monitor"
      },
      {
        "automaton": "sender"
      },
      {
        "automaton": "receiver"
      },
      {
        "automaton": "channelK"
      },
      {
        "automaton": "channelL"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "S_in",
          "S_in",
          null,
          null,
          null
        ],
        "result": "S_in"
      },
      {
        "synchronise": [
          "sndD",
          "sndD",
          null,
          "sndD",
          null
        ],
        "result": "sndD"
      },
      {
        "synchronise": [
          null,
          "rcvA",
          null,
          null,
          "rcvA"
        ],
        "result": "rcvA"
      },
      {
        "synchronise": [
          null,
          "S_DK",
          null,
          null,
          null
        ],
        "result": "S_DK"
      },
      {
        "synchronise": [
          null,
          "S_NOK",
          null,
          null,
          null
        ],
        "result": "S_NOK"
      },
      {
        "synchronise": [
          null,
          "S_OK",
          null,
          null,
          null
        ],
        "result": "S_OK"
      },
      {
        "synchronise": [
          null,
          null,
          "rcvD",
          "rcvD",
          null
        ],
        "result": "rcvD"
      },
      {
        "synchronise": [
          null,
          null,
          "sndA",
          null,
          "sndA"
        ],
        "result": "sndA"
      },
      {
        "synchronise": [
          null,
          null,
          "R_NOK",
          null,
          null
        ],
        "result": "R_NOK"
      },
      {
        "synchronise": [
          null,
          null,
          "R_OK",
          null,
          null
        ],
        "result": "R_OK"
      },
      {
        "synchronise": [
          null,
          null,
          "R_FST",
          null,
          null
        ],
        "result": "R_FST"
      },
      {
        "synchronise": [
          null,
          null,
          "R_INC",
          null,
          null
        ],
        "result": "R_INC"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          "lostK",
          null
        ],
        "result": "lostK"
      },
      {
        "synchronise": [
          null,
          null,
          null,
          null,
          "lostL"
        ],
        "result": "lostL"
      }
    ]
  }
}