{
  "jani-version": 1,
  "name": "Researcher/researcher.imi",
  "type": "sha",
  "features": [
    "derived-operators"
  ],
  "actions": [
    {
      "name": "done"
    },
    {
      "name": "drink"
    },
    {
      "name": "drunk"
    },
    {
      "name": "restart"
    }
  ],
  "variables": [
    {
      "name": "x",
      "type": "continuous",
      "initial_value": 0
    },
    {
      "name": "t",
      "type": "continuous",
      "initial_value": 0
    },
    {
      "name": "nb",
      "type": "real",
      "initial_value": 0
    },
    {
      "name": "pTotal",
      "type": "real"
    },
    {
      "name": "pNeed",
      "type": "real"
    },
    {
      "name": "MAXBREAK",
      "type": "real"
    },
    {
      "name": "pCoffee",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "researcher",
      "locations": [
        {
          "name": "working",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "pTotal",
                "right": "x"
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "t"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "workingFast",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "pTotal",
                "right": "x"
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 2
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "t"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "coffeeing",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "pCoffee",
                "right": "t"
              },
              "right": {
                "op": "∧",
                "left": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "x"
                  },
                  "right": 1
                },
                "right": {
                  "op": "=",
                  "left": {
                    "op": "der",
                    "var": "t"
                  },
                  "right": 1
                }
              }
            }
          }
        },
        {
          "name": "finished",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "x"
                },
                "right": 1
              },
              "right": {
                "op": "=",
                "left": {
                  "op": "der",
                  "var": "t"
                },
                "right": 1
              }
            }
          }
        }
      ],
      "initial_locations": [
        "working"
      ],
      "edges": [
        {
          "location": "working",
          "guard": {
            "op": ">",
            "left": {
              "op": "*",
              "left": 5,
              "right": "x"
            },
            "right": {
              "op": "*",
              "left": 4,
              "right": "pTotal"
            }
          },
          "destinations": [
            {
              "location": "workingFast"
            }
          ]
        },
        {
          "location": "working",
          "guard": {
            "op": "=",
            "left": "pTotal",
            "right": "x"
          },
          "destinations": [
            {
              "location": "finished",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "t",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "working",
          "guard": {
            "op": "∧",
            "left": {
              "op": ">",
              "left": "t",
              "right": "pNeed"
            },
            "right": {
              "op": ">",
              "left": "MAXBREAK",
              "right": {
                "op": "+",
                "left": 1,
                "right": "nb"
              }
            }
          },
          "destinations": [
            {
              "location": "coffeeing",
              "assignments": [
                {
                  "ref": "t",
                  "value": 0
                },
                {
                  "ref": "nb",
                  "value": {
                    "op": "+",
                    "left": "nb",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "workingFast",
          "destinations": [
            {
              "location": "working"
            }
          ]
        },
        {
          "location": "workingFast",
          "guard": {
            "op": "=",
            "left": "pTotal",
            "right": "x"
          },
          "destinations": [
            {
              "location": "finished",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "t",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "workingFast",
          "guard": {
            "op": "∧",
            "left": {
              "op": ">",
              "left": {
                "op": "*",
                "left": 5,
                "right": "t"
              },
              "right": {
                "op": "*",
                "left": 3,
                "right": "pNeed"
              }
            },
            "right": {
              "op": ">",
              "left": "MAXBREAK",
              "right": {
                "op": "+",
                "left": 1,
                "right": "nb"
              }
            }
          },
          "destinations": [
            {
              "location": "coffeeing",
              "assignments": [
                {
                  "ref": "t",
                  "value": 0
                },
                {
                  "ref": "nb",
                  "value": {
                    "op": "+",
                    "left": "nb",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "coffeeing",
          "guard": {
            "op": "∧",
            "left": {
              "op": "=",
              "left": "pCoffee",
              "right": "t"
            },
            "right": {
              "op": ">",
              "left": {
                "op": "*",
                "left": 5,
                "right": "x"
              },
              "right": {
                "op": "*",
                "left": 4,
                "right": "pTotal"
              }
            }
          },
          "destinations": [
            {
              "location": "workingFast",
              "assignments": [
                {
                  "ref": "t",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "coffeeing",
          "guard": {
            "op": "=",
            "left": "pCoffee",
            "right": "t"
          },
          "destinations": [
            {
              "location": "working",
              "assignments": [
                {
                  "ref": "t",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "finished",
          "destinations": [
            {
              "location": "working",
              "assignments": [
                {
                  "ref": "x",
                  "value": 0
                },
                {
                  "ref": "t",
                  "value": {
                    "op": "+",
                    "left": {
                      "op": "*",
                      "left": {
                        "op": "/",
                        "left": 1,
                        "right": 2
                      },
                      "right": "pNeed"
                    },
                    "right": 0
                  }
                },
                {
                  "ref": "nb",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "researcher"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "done"
        ],
        "result": "done"
      },
      {
        "synchronise": [
          "drink"
        ],
        "result": "drink"
      },
      {
        "synchronise": [
          "drunk"
        ],
        "result": "drunk"
      },
      {
        "synchronise": [
          "restart"
        ],
        "result": "restart"
      }
    ]
  }
}