{
  "jani-version": 1,
  "name": "Therac/therac25.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "key_E"
    },
    {
      "name": "key_X"
    },
    {
      "name": "key_enter"
    },
    {
      "name": "key_up"
    },
    {
      "name": "copy_25MV"
    },
    {
      "name": "copy_25MeV"
    },
    {
      "name": "send_25MV"
    },
    {
      "name": "send_25MeV"
    }
  ],
  "variables": [
    {
      "name": "x_engineer",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "x_buffer",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "buffer_VT100",
      "type": "int",
      "initial-value": 2
    },
    {
      "name": "buffer_PDP11",
      "type": "int",
      "initial-value": 2
    },
    {
      "name": "p_key",
      "type": "real"
    },
    {
      "name": "p_period",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "engineer",
      "locations": [
        {
          "name": "engineer_idle"
        },
        {
          "name": "engineer_correct1"
        },
        {
          "name": "engineer_correct2"
        },
        {
          "name": "engineer_incorrect1"
        },
        {
          "name": "engineer_incorrect2"
        },
        {
          "name": "engineer_incorrect3"
        },
        {
          "name": "engineer_incorrect4"
        }
      ],
      "initial-locations": [
        "engineer_idle"
      ],
      "edges": [
        {
          "location": "engineer_idle",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": 30
            }
          },
          "destinations": [
            {
              "location": "engineer_correct1",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_idle",
          "action": "nosync_2",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": 30
            }
          },
          "destinations": [
            {
              "location": "engineer_incorrect1",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_correct1",
          "action": "key_E",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_correct2",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_correct2",
          "action": "key_enter",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_idle",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_incorrect1",
          "action": "key_X",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_incorrect2",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_incorrect2",
          "action": "key_up",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_incorrect3",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_incorrect3",
          "action": "key_E",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_incorrect4",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "engineer_incorrect4",
          "action": "key_enter",
          "guard": {
            "exp": {
              "op": ">",
              "left": "x_engineer",
              "right": "p_key"
            }
          },
          "destinations": [
            {
              "location": "engineer_idle",
              "assignments": [
                {
                  "ref": "x_engineer",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "buffer_copier",
      "locations": [
        {
          "name": "loc_buffer_copier",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": "p_period",
              "right": "x_buffer"
            }
          }
        }
      ],
      "initial-locations": [
        "loc_buffer_copier"
      ],
      "edges": [
        {
          "location": "loc_buffer_copier",
          "action": "copy_25MV",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer_VT100",
                "right": 1
              },
              "right": {
                "op": "=",
                "left": "p_period",
                "right": "x_buffer"
              }
            }
          },
          "destinations": [
            {
              "location": "loc_buffer_copier",
              "assignments": [
                {
                  "ref": "buffer_PDP11",
                  "value": 1
                },
                {
                  "ref": "x_buffer",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "loc_buffer_copier",
          "action": "copy_25MeV",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "buffer_VT100",
                "right": 2
              },
              "right": {
                "op": "=",
                "left": "p_period",
                "right": "x_buffer"
              }
            }
          },
          "destinations": [
            {
              "location": "loc_buffer_copier",
              "assignments": [
                {
                  "ref": "buffer_PDP11",
                  "value": 2
                },
                {
                  "ref": "x_buffer",
                  "value": 0
                }
              ]
            }
          ]
        }
      ]
    },
    {
      "name": "PDP11",
      "locations": [
        {
          "name": "loc_PDP11"
        },
        {
          "name": "loc_PDP11_send"
        }
      ],
      "initial-locations": [
        "loc_PDP11"
      ],
      "edges": [
        {
          "location": "loc_PDP11",
          "action": "key_X",
          "destinations": [
            {
              "location": "loc_PDP11",
              "assignments": [
                {
                  "ref": "buffer_VT100",
                  "value": 1
                }
              ]
            }
          ]
        },
        {
          "location": "loc_PDP11",
          "action": "key_E",
          "destinations": [
            {
              "location": "loc_PDP11",
              "assignments": [
                {
                  "ref": "buffer_VT100",
                  "value": 2
                }
              ]
            }
          ]
        },
        {
          "location": "loc_PDP11",
          "action": "key_enter",
          "destinations": [
            {
              "location": "loc_PDP11_send"
            }
          ]
        },
        {
          "location": "loc_PDP11_send",
          "action": "send_25MV",
          "guard": {
            "exp": {
              "op": "=",
              "left": "buffer_PDP11",
              "right": 1
            }
          },
          "destinations": [
            {
              "location": "loc_PDP11"
            }
          ]
        },
        {
          "location": "loc_PDP11_send",
          "action": "send_25MeV",
          "guard": {
            "exp": {
              "op": "=",
              "left": "buffer_PDP11",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "loc_PDP11"
            }
          ]
        }
      ]
    },
    {
      "name": "observer",
      "locations": [
        {
          "name": "obs_ok"
        },
        {
          "name": "obs_nok"
        }
      ],
      "initial-locations": [
        "obs_ok"
      ],
      "edges": [
        {
          "location": "obs_ok",
          "action": "send_25MV",
          "destinations": [
            {
              "location": "obs_nok"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "engineer"
      },
      {
        "automaton": "buffer_copier"
      },
      {
        "automaton": "PDP11"
      },
      {
        "automaton": "observer"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "key_E",
          null,
          "key_E",
          null
        ],
        "result": "key_E"
      },
      {
        "synchronise": [
          "key_X",
          null,
          "key_X",
          null
        ],
        "result": "key_X"
      },
      {
        "synchronise": [
          "key_enter",
          null,
          "key_enter",
          null
        ],
        "result": "key_enter"
      },
      {
        "synchronise": [
          "key_up",
          null,
          null,
          null
        ],
        "result": "key_up"
      },
      {
        "synchronise": [
          null,
          "copy_25MV",
          null,
          null
        ],
        "result": "copy_25MV"
      },
      {
        "synchronise": [
          null,
          "copy_25MeV",
          null,
          null
        ],
        "result": "copy_25MeV"
      },
      {
        "synchronise": [
          null,
          null,
          "send_25MV",
          "send_25MV"
        ],
        "result": "send_25MV"
      },
      {
        "synchronise": [
          null,
          null,
          "send_25MeV",
          null
        ],
        "result": "send_25MeV"
      }
    ]
  }
}