{
  "jani-version": 1,
  "name": "Coffee/CoffeeDrinker/coffeeDrinker.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "press"
    },
    {
      "name": "cup"
    },
    {
      "name": "coffee"
    },
    {
      "name": "sleep"
    }
  ],
  "variables": [
    {
      "name": "x1",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "x2",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "y1",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "y2",
      "type": "clock",
      "initial_value": 0
    },
    {
      "name": "nb_sugar",
      "type": "int",
      "initial_value": 0
    },
    {
      "name": "p_add_sugar",
      "type": "real"
    },
    {
      "name": "p_coffee",
      "type": "real"
    },
    {
      "name": "p_work_min",
      "type": "real"
    },
    {
      "name": "p_work_max",
      "type": "real"
    },
    {
      "name": "p_press_min",
      "type": "real"
    },
    {
      "name": "p_patience_max",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "machine",
      "locations": [
        {
          "name": "idle"
        },
        {
          "name": "add_sugar",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p_add_sugar",
                "right": "x2"
              },
              "right": {
                "op": ">",
                "left": "p_coffee",
                "right": "x2"
              }
            }
          }
        },
        {
          "name": "preparing_coffee",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_coffee",
              "right": "x2"
            }
          }
        },
        {
          "name": "cdone",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x1"
            }
          }
        }
      ],
      "initial_locations": [
        "idle"
      ],
      "edges": [
        {
          "location": "idle",
          "destinations": [
            {
              "location": "add_sugar",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "x2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "add_sugar",
          "destinations": [
            {
              "location": "add_sugar",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "add_sugar",
          "guard": {
            "op": "=",
            "left": "p_add_sugar",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "preparing_coffee"
            }
          ]
        },
        {
          "location": "preparing_coffee",
          "destinations": [
            {
              "location": "preparing_coffee"
            }
          ]
        },
        {
          "location": "preparing_coffee",
          "guard": {
            "op": "=",
            "left": "p_coffee",
            "right": "x2"
          },
          "destinations": [
            {
              "location": "cdone",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "cdone",
          "destinations": [
            {
              "location": "add_sugar",
              "assignments": [
                {
                  "ref": "x1",
                  "value": 0
                },
                {
                  "ref": "x2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "cdone",
          "guard": {
            "op": "=",
            "left": "x1",
            "right": 10
          },
          "destinations": [
            {
              "location": "idle"
            }
          ]
        }
      ]
    },
    {
      "name": "researcher",
      "locations": [
        {
          "name": "researching",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_work_max",
              "right": "y1"
            }
          }
        },
        {
          "name": "add_sugar",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "≤",
                "left": "nb_sugar",
                "right": 3
              },
              "right": {
                "op": ">",
                "left": "p_patience_max",
                "right": "y2"
              }
            }
          }
        },
        {
          "name": "wait_coffee",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_patience_max",
              "right": "y2"
            }
          }
        },
        {
          "name": "mad"
        }
      ],
      "initial_locations": [
        "researching"
      ],
      "edges": [
        {
          "location": "researching",
          "guard": {
            "op": ">",
            "left": "y1",
            "right": "p_work_min"
          },
          "destinations": [
            {
              "location": "add_sugar",
              "assignments": [
                {
                  "ref": "y1",
                  "value": 0
                },
                {
                  "ref": "y2",
                  "value": 0
                },
                {
                  "ref": "nb_sugar",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "add_sugar",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "nb_sugar",
              "right": {
                "op": " - ",
                "left": 3,
                "right": 1
              }
            },
            "right": {
              "op": ">",
              "left": "y1",
              "right": "p_press_min"
            }
          },
          "destinations": [
            {
              "location": "wait_coffee",
              "assignments": [
                {
                  "ref": "y1",
                  "value": 0
                },
                {
                  "ref": "nb_sugar",
                  "value": {
                    "op": " + ",
                    "left": "nb_sugar",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "add_sugar",
          "guard": {
            "op": "∧",
            "left": {
              "op": "<",
              "left": "nb_sugar",
              "right": {
                "op": " - ",
                "left": 3,
                "right": 1
              }
            },
            "right": {
              "op": ">",
              "left": "y1",
              "right": "p_press_min"
            }
          },
          "destinations": [
            {
              "location": "add_sugar",
              "assignments": [
                {
                  "ref": "y1",
                  "value": 0
                },
                {
                  "ref": "nb_sugar",
                  "value": {
                    "op": " + ",
                    "left": "nb_sugar",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "add_sugar",
          "destinations": [
            {
              "location": "wait_coffee"
            }
          ]
        },
        {
          "location": "add_sugar",
          "guard": {
            "op": "=",
            "left": "p_patience_max",
            "right": "y2"
          },
          "destinations": [
            {
              "location": "mad"
            }
          ]
        },
        {
          "location": "wait_coffee",
          "guard": {
            "op": "≥",
            "left": "p_patience_max",
            "right": "y2"
          },
          "destinations": [
            {
              "location": "researching",
              "assignments": [
                {
                  "ref": "y1",
                  "value": 0
                },
                {
                  "ref": "y2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "wait_coffee",
          "guard": {
            "op": "=",
            "left": "p_patience_max",
            "right": "y2"
          },
          "destinations": [
            {
              "location": "mad"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "machine"
      },
      {
        "automaton": "researcher"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "press",
          "press"
        ],
        "result": "press"
      },
      {
        "synchronise": [
          "cup",
          null
        ],
        "result": "cup"
      },
      {
        "synchronise": [
          "coffee",
          "coffee"
        ],
        "result": "coffee"
      },
      {
        "synchronise": [
          "sleep",
          null
        ],
        "result": "sleep"
      }
    ]
  }
}