{
  "jani-version": 1,
  "name": "Merging/crossing_signals/crossing_signals-20.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "satisfied"
    },
    {
      "name": "greater"
    },
    {
      "name": "smaller"
    },
    {
      "name": "decrease_slow_1"
    },
    {
      "name": "stabilize_1"
    },
    {
      "name": "increase_slow_1"
    },
    {
      "name": "decrease_slow_2"
    },
    {
      "name": "stabilize_2"
    },
    {
      "name": "increase_slow_2"
    }
  ],
  "variables": [
    {
      "name": "x",
      "type": "continuous",
      "initial-value": 0
    },
    {
      "name": "s_1",
      "type": "continuous",
      "initial-value": 0
    },
    {
      "name": "s_2",
      "type": "continuous",
      "initial-value": 0
    },
    {
      "name": "nb",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "p",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "spec",
      "locations": [
        {
          "name": "l1",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "x"
                },
                "right": 1
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "l2",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "x"
                },
                "right": 1
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "wait10",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p",
                "right": "x"
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "∧",
                  "left": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "s_1"
                    },
                    "right": 1
                  },
                  "right": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "s_2"
                    },
                    "right": 1
                  }
                }
              }
            }
          }
        },
        {
          "name": "lfinal",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "x"
                },
                "right": 1
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": 1
                }
              }
            }
          }
        }
      ],
      "initial-locations": [
        "l1"
      ],
      "edges": [
        {
          "location": "l1",
          "action": "greater",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "s_1",
              "right": "s_2"
            }
          },
          "destinations": [
            {
              "location": "l2"
            }
          ]
        },
        {
          "location": "l2",
          "action": "smaller",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "nb",
                "right": 20
              },
              "right": {
                "op": "≥",
                "left": "s_2",
                "right": "s_1"
              }
            }
          },
          "destinations": [
            {
              "location": "wait10",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "l2",
          "action": "smaller",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "<",
                "left": "nb",
                "right": 20
              },
              "right": {
                "op": "≥",
                "left": "s_2",
                "right": "s_1"
              }
            }
          },
          "destinations": [
            {
              "location": "l1",
              "assignments": [
                {
                  "ref": "nb",
                  "value": {
                    "op": "+",
                    "left": "nb",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "wait10",
          "action": "satisfied",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "p",
                "right": "x"
              },
              "right": {
                "op": "=",
                "left": "s_1",
                "right": {
                  "op": "*",
                  "left": 3,
                  "right": "s_2"
                }
              }
            }
          },
          "destinations": [
            {
              "location": "lfinal"
            }
          ]
        }
      ]
    },
    {
      "name": "signal_1",
      "locations": [
        {
          "name": "increasing_slow",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "s_1"
                },
                "right": 1
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "stabilized",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "s_1"
                },
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "decreasing_slow",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "s_1",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": -1
                },
                "right": {
                  "op": "∧",
                  "left": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "x"
                    },
                    "right": 1
                  },
                  "right": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "s_2"
                    },
                    "right": 1
                  }
                }
              }
            }
          }
        }
      ],
      "initial-locations": [
        "stabilized"
      ],
      "edges": [
        {
          "location": "increasing_slow",
          "action": "stabilize_1",
          "destinations": [
            {
              "location": "stabilized"
            }
          ]
        },
        {
          "location": "stabilized",
          "action": "increase_slow_1",
          "destinations": [
            {
              "location": "increasing_slow"
            }
          ]
        },
        {
          "location": "stabilized",
          "action": "decrease_slow_1",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "s_1",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "decreasing_slow"
            }
          ]
        },
        {
          "location": "decreasing_slow",
          "action": "stabilize_1",
          "destinations": [
            {
              "location": "stabilized"
            }
          ]
        }
      ]
    },
    {
      "name": "signal_2",
      "locations": [
        {
          "name": "increasing_slow",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "s_2"
                },
                "right": 1
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "stabilized",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "s_2"
                },
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_1"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "decreasing_slow",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "s_2",
                "right": 0
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "s_2"
                  },
                  "right": -1
                },
                "right": {
                  "op": "∧",
                  "left": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "x"
                    },
                    "right": 1
                  },
                  "right": {
                    "op": "=",
                    "left": {
                      "op": "der",
                      "var": "s_1"
                    },
                    "right": 1
                  }
                }
              }
            }
          }
        }
      ],
      "initial-locations": [
        "stabilized"
      ],
      "edges": [
        {
          "location": "increasing_slow",
          "action": "stabilize_2",
          "destinations": [
            {
              "location": "stabilized"
            }
          ]
        },
        {
          "location": "stabilized",
          "action": "increase_slow_2",
          "destinations": [
            {
              "location": "increasing_slow"
            }
          ]
        },
        {
          "location": "stabilized",
          "action": "decrease_slow_2",
          "guard": {
            "exp": {
              "op": "≥",
              "left": "s_2",
              "right": 0
            }
          },
          "destinations": [
            {
              "location": "decreasing_slow"
            }
          ]
        },
        {
          "location": "decreasing_slow",
          "action": "stabilize_2",
          "destinations": [
            {
              "location": "stabilized"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "spec"
      },
      {
        "automaton": "signal_1"
      },
      {
        "automaton": "signal_2"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "satisfied",
          null,
          null
        ],
        "result": "satisfied"
      },
      {
        "synchronise": [
          "greater",
          null,
          null
        ],
        "result": "greater"
      },
      {
        "synchronise": [
          "smaller",
          null,
          null
        ],
        "result": "smaller"
      },
      {
        "synchronise": [
          null,
          "decrease_slow_1",
          null
        ],
        "result": "decrease_slow_1"
      },
      {
        "synchronise": [
          null,
          "stabilize_1",
          null
        ],
        "result": "stabilize_1"
      },
      {
        "synchronise": [
          null,
          "increase_slow_1",
          null
        ],
        "result": "increase_slow_1"
      },
      {
        "synchronise": [
          null,
          null,
          "decrease_slow_2"
        ],
        "result": "decrease_slow_2"
      },
      {
        "synchronise": [
          null,
          null,
          "stabilize_2"
        ],
        "result": "stabilize_2"
      },
      {
        "synchronise": [
          null,
          null,
          "increase_slow_2"
        ],
        "result": "increase_slow_2"
      }
    ]
  }
}