{
  "jani-version": 1,
  "name": "Security/ATM_PTO/ATM_PTO.imi",
  "type": "sha",
  "features": [
    "derived-operators",
    "arrays",
    "datatypes",
    "functions"
  ],
  "datatypes": [
    {
      "name": "binary_word",
      "members": [
        {
          "name": "elements",
          "type": {
            "kind": "array",
            "base": "bool"
          }
        }
      ]
    }
  ],
  "functions": [],
  "actions": [
    {
      "name": "askPassword_1"
    },
    {
      "name": "finish"
    },
    {
      "name": "start_1"
    },
    {
      "name": "displayBalance_1"
    },
    {
      "name": "press_OK_1"
    },
    {
      "name": "quickWithdrawal_1"
    },
    {
      "name": "restart_1"
    },
    {
      "name": "correctAmount_1"
    },
    {
      "name": "correctPassword_1"
    },
    {
      "name": "press_finish_1"
    },
    {
      "name": "incorrectAmount_1"
    },
    {
      "name": "incorrectPassword_1"
    },
    {
      "name": "normalWithdrawal_1"
    },
    {
      "name": "take_cash_1"
    },
    {
      "name": "askPassword_2"
    },
    {
      "name": "start_2"
    },
    {
      "name": "displayBalance_2"
    },
    {
      "name": "press_OK_2"
    },
    {
      "name": "quickWithdrawal_2"
    },
    {
      "name": "restart_2"
    },
    {
      "name": "correctAmount_2"
    },
    {
      "name": "correctPassword_2"
    },
    {
      "name": "press_finish_2"
    },
    {
      "name": "incorrectAmount_2"
    },
    {
      "name": "incorrectPassword_2"
    },
    {
      "name": "normalWithdrawal_2"
    },
    {
      "name": "take_cash_2"
    }
  ],
  "variables": [
    {
      "name": "x_1",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "y_1",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "x_2",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "y_2",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "t_total",
      "type": "clock",
      "initial-value": 0
    },
    {
      "name": "cash_spotted_1",
      "type": "bool",
      "initial-value": false
    },
    {
      "name": "cash_spotted_2",
      "type": "bool",
      "initial-value": false
    },
    {
      "name": "nbFailedPassword_1",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "nbFailedAmount_1",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "nbRestart_1",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "nbFailedPassword_2",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "nbFailedAmount_2",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "nbRestart_2",
      "type": "int",
      "initial-value": 0
    },
    {
      "name": "p_total",
      "type": "real"
    }
  ],
  "properties": [],
  "automata": [
    {
      "name": "ATM_1",
      "locations": [
        {
          "name": "initial"
        },
        {
          "name": "welcome",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 3,
              "right": "x_1"
            }
          }
        },
        {
          "name": "waitingPassword",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_1"
            }
          }
        },
        {
          "name": "waitChoice",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_1"
            }
          }
        },
        {
          "name": "preparingWithdrawalQuick",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 15,
              "right": "x_1"
            }
          }
        },
        {
          "name": "moneyAvailableQuick",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 20,
              "right": "x_1"
            }
          }
        },
        {
          "name": "choosingAmount",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 12,
              "right": "x_1"
            }
          }
        },
        {
          "name": "preparingWithdrawalNormal",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 15,
              "right": "x_1"
            }
          }
        },
        {
          "name": "moneyAvailableNormal",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 20,
              "right": "x_1"
            }
          }
        },
        {
          "name": "otherOperation",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_1"
            }
          }
        },
        {
          "name": "displayingBalance",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_1"
            }
          }
        },
        {
          "name": "terminating",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p_total",
                "right": "y_1"
              },
              "right": {
                "op": ">",
                "left": "p_total",
                "right": "t_total"
              }
            }
          }
        },
        {
          "name": "cancelling",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p_total",
                "right": "y_1"
              },
              "right": {
                "op": ">",
                "left": "p_total",
                "right": "t_total"
              }
            }
          }
        },
        {
          "name": "the_end"
        }
      ],
      "initial-locations": [
        "initial"
      ],
      "edges": [
        {
          "location": "initial",
          "action": "start_1",
          "destinations": [
            {
              "location": "welcome",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "y_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "welcome",
          "action": "askPassword_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 3
            }
          },
          "destinations": [
            {
              "location": "waitingPassword",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "nosync_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "correctPassword_1",
          "destinations": [
            {
              "location": "waitChoice",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "incorrectPassword_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "nbFailedPassword_1",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "cancelling",
              "assignments": [
                {
                  "ref": "nbFailedPassword_1",
                  "value": {
                    "op": "+",
                    "left": "nbFailedPassword_1",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "incorrectPassword_1",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbFailedPassword_1",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "waitingPassword",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "nbFailedPassword_1",
                  "value": {
                    "op": "+",
                    "left": "nbFailedPassword_1",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "nosync_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "quickWithdrawal_1",
          "destinations": [
            {
              "location": "preparingWithdrawalQuick",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "normalWithdrawal_1",
          "destinations": [
            {
              "location": "choosingAmount",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "displayBalance_1",
          "destinations": [
            {
              "location": "displayingBalance",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "preparingWithdrawalQuick",
          "action": "nosync_3",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 15
            }
          },
          "destinations": [
            {
              "location": "moneyAvailableQuick",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableQuick",
          "action": "take_cash_1",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "∨",
                "left": "cash_spotted_1",
                "right": {
                  "op": "¬",
                  "exp": "cash_spotted_1"
                }
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end",
              "assignments": [
                {
                  "ref": "cash_spotted_1",
                  "value": true
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableQuick",
          "action": "nosync_4",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 20
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "nosync_5",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 12
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "correctAmount_1",
          "destinations": [
            {
              "location": "preparingWithdrawalNormal",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "incorrectAmount_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "nbFailedAmount_1",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "cancelling",
              "assignments": [
                {
                  "ref": "nbFailedAmount_1",
                  "value": {
                    "op": "+",
                    "left": "nbFailedAmount_1",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "incorrectAmount_1",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbFailedAmount_1",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "choosingAmount",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "nbFailedAmount_1",
                  "value": {
                    "op": "+",
                    "left": "nbFailedAmount_1",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "preparingWithdrawalNormal",
          "action": "nosync_6",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 15
            }
          },
          "destinations": [
            {
              "location": "moneyAvailableNormal",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableNormal",
          "action": "take_cash_1",
          "destinations": [
            {
              "location": "otherOperation",
              "assignments": [
                {
                  "ref": "cash_spotted_1",
                  "value": true
                },
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableNormal",
          "action": "nosync_7",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 20
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "press_finish_1",
          "destinations": [
            {
              "location": "terminating"
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "restart_1",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbRestart_1",
              "right": 1
            }
          },
          "destinations": [
            {
              "location": "waitChoice",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                },
                {
                  "ref": "y_1",
                  "value": 0
                },
                {
                  "ref": "nbRestart_1",
                  "value": {
                    "op": "+",
                    "left": "nbRestart_1",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "nosync_8",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "terminating"
            }
          ]
        },
        {
          "location": "displayingBalance",
          "action": "press_OK_1",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_total",
              "right": "t_total"
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        },
        {
          "location": "displayingBalance",
          "action": "nosync_9",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_1",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "otherOperation",
              "assignments": [
                {
                  "ref": "x_1",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "terminating",
          "action": "finish",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "p_total",
                "right": "y_1"
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        },
        {
          "location": "cancelling",
          "action": "finish",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "p_total",
                "right": "y_1"
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        }
      ]
    },
    {
      "name": "ATM_2",
      "locations": [
        {
          "name": "initial"
        },
        {
          "name": "welcome",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 3,
              "right": "x_2"
            }
          }
        },
        {
          "name": "waitingPassword",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_2"
            }
          }
        },
        {
          "name": "waitChoice",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_2"
            }
          }
        },
        {
          "name": "preparingWithdrawalQuick",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 15,
              "right": "x_2"
            }
          }
        },
        {
          "name": "moneyAvailableQuick",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 20,
              "right": "x_2"
            }
          }
        },
        {
          "name": "choosingAmount",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 12,
              "right": "x_2"
            }
          }
        },
        {
          "name": "preparingWithdrawalNormal",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 15,
              "right": "x_2"
            }
          }
        },
        {
          "name": "moneyAvailableNormal",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 20,
              "right": "x_2"
            }
          }
        },
        {
          "name": "otherOperation",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_2"
            }
          }
        },
        {
          "name": "displayingBalance",
          "time-progress": {
            "exp": {
              "op": ">",
              "left": 10,
              "right": "x_2"
            }
          }
        },
        {
          "name": "terminating",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p_total",
                "right": "y_2"
              },
              "right": {
                "op": ">",
                "left": "p_total",
                "right": "t_total"
              }
            }
          }
        },
        {
          "name": "cancelling",
          "time-progress": {
            "exp": {
              "op": "∧",
              "left": {
                "op": ">",
                "left": "p_total",
                "right": "y_2"
              },
              "right": {
                "op": ">",
                "left": "p_total",
                "right": "t_total"
              }
            }
          }
        },
        {
          "name": "the_end"
        }
      ],
      "initial-locations": [
        "initial"
      ],
      "edges": [
        {
          "location": "initial",
          "action": "start_2",
          "destinations": [
            {
              "location": "welcome",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "y_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "welcome",
          "action": "askPassword_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 3
            }
          },
          "destinations": [
            {
              "location": "waitingPassword",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "nosync_10",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "correctPassword_2",
          "destinations": [
            {
              "location": "waitChoice",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "incorrectPassword_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "nbFailedPassword_2",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "cancelling",
              "assignments": [
                {
                  "ref": "nbFailedPassword_2",
                  "value": {
                    "op": "+",
                    "left": "nbFailedPassword_2",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "waitingPassword",
          "action": "incorrectPassword_2",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbFailedPassword_2",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "waitingPassword",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "nbFailedPassword_2",
                  "value": {
                    "op": "+",
                    "left": "nbFailedPassword_2",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "nosync_11",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "quickWithdrawal_2",
          "destinations": [
            {
              "location": "preparingWithdrawalQuick",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "normalWithdrawal_2",
          "destinations": [
            {
              "location": "choosingAmount",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "waitChoice",
          "action": "displayBalance_2",
          "destinations": [
            {
              "location": "displayingBalance",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "preparingWithdrawalQuick",
          "action": "nosync_12",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 15
            }
          },
          "destinations": [
            {
              "location": "moneyAvailableQuick",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableQuick",
          "action": "take_cash_2",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "∨",
                "left": "cash_spotted_2",
                "right": {
                  "op": "¬",
                  "exp": "cash_spotted_2"
                }
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end",
              "assignments": [
                {
                  "ref": "cash_spotted_2",
                  "value": true
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableQuick",
          "action": "nosync_13",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 20
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "nosync_14",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 12
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "correctAmount_2",
          "destinations": [
            {
              "location": "preparingWithdrawalNormal",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "incorrectAmount_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "nbFailedAmount_2",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "cancelling",
              "assignments": [
                {
                  "ref": "nbFailedAmount_2",
                  "value": {
                    "op": "+",
                    "left": "nbFailedAmount_2",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "choosingAmount",
          "action": "incorrectAmount_2",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbFailedAmount_2",
              "right": 2
            }
          },
          "destinations": [
            {
              "location": "choosingAmount",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "nbFailedAmount_2",
                  "value": {
                    "op": "+",
                    "left": "nbFailedAmount_2",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "preparingWithdrawalNormal",
          "action": "nosync_15",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 15
            }
          },
          "destinations": [
            {
              "location": "moneyAvailableNormal",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableNormal",
          "action": "take_cash_2",
          "destinations": [
            {
              "location": "otherOperation",
              "assignments": [
                {
                  "ref": "cash_spotted_2",
                  "value": true
                },
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "moneyAvailableNormal",
          "action": "nosync_16",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 20
            }
          },
          "destinations": [
            {
              "location": "cancelling"
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "press_finish_2",
          "destinations": [
            {
              "location": "terminating"
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "restart_2",
          "guard": {
            "exp": {
              "op": "<",
              "left": "nbRestart_2",
              "right": 1
            }
          },
          "destinations": [
            {
              "location": "waitChoice",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                },
                {
                  "ref": "y_2",
                  "value": 0
                },
                {
                  "ref": "nbRestart_2",
                  "value": {
                    "op": "+",
                    "left": "nbRestart_2",
                    "right": 1
                  }
                }
              ]
            }
          ]
        },
        {
          "location": "otherOperation",
          "action": "nosync_17",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "terminating"
            }
          ]
        },
        {
          "location": "displayingBalance",
          "action": "press_OK_2",
          "guard": {
            "exp": {
              "op": "=",
              "left": "p_total",
              "right": "t_total"
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        },
        {
          "location": "displayingBalance",
          "action": "nosync_18",
          "guard": {
            "exp": {
              "op": "=",
              "left": "x_2",
              "right": 10
            }
          },
          "destinations": [
            {
              "location": "otherOperation",
              "assignments": [
                {
                  "ref": "x_2",
                  "value": 0
                }
              ]
            }
          ]
        },
        {
          "location": "terminating",
          "action": "finish",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "p_total",
                "right": "y_2"
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        },
        {
          "location": "cancelling",
          "action": "finish",
          "guard": {
            "exp": {
              "op": "∧",
              "left": {
                "op": "=",
                "left": "p_total",
                "right": "y_2"
              },
              "right": {
                "op": "=",
                "left": "p_total",
                "right": "t_total"
              }
            }
          },
          "destinations": [
            {
              "location": "the_end"
            }
          ]
        }
      ]
    }
  ],
  "system": {
    "elements": [
      {
        "automaton": "ATM_1"
      },
      {
        "automaton": "ATM_2"
      }
    ],
    "syncs": [
      {
        "synchronise": [
          "askPassword_1",
          null
        ],
        "result": "askPassword_1"
      },
      {
        "synchronise": [
          "finish",
          "finish"
        ],
        "result": "finish"
      },
      {
        "synchronise": [
          "start_1",
          null
        ],
        "result": "start_1"
      },
      {
        "synchronise": [
          "displayBalance_1",
          null
        ],
        "result": "displayBalance_1"
      },
      {
        "synchronise": [
          "press_OK_1",
          null
        ],
        "result": "press_OK_1"
      },
      {
        "synchronise": [
          "quickWithdrawal_1",
          null
        ],
        "result": "quickWithdrawal_1"
      },
      {
        "synchronise": [
          "restart_1",
          null
        ],
        "result": "restart_1"
      },
      {
        "synchronise": [
          "correctAmount_1",
          null
        ],
        "result": "correctAmount_1"
      },
      {
        "synchronise": [
          "correctPassword_1",
          null
        ],
        "result": "correctPassword_1"
      },
      {
        "synchronise": [
          "press_finish_1",
          null
        ],
        "result": "press_finish_1"
      },
      {
        "synchronise": [
          "incorrectAmount_1",
          null
        ],
        "result": "incorrectAmount_1"
      },
      {
        "synchronise": [
          "incorrectPassword_1",
          null
        ],
        "result": "incorrectPassword_1"
      },
      {
        "synchronise": [
          "normalWithdrawal_1",
          null
        ],
        "result": "normalWithdrawal_1"
      },
      {
        "synchronise": [
          "take_cash_1",
          null
        ],
        "result": "take_cash_1"
      },
      {
        "synchronise": [
          null,
          "askPassword_2"
        ],
        "result": "askPassword_2"
      },
      {
        "synchronise": [
          null,
          "start_2"
        ],
        "result": "start_2"
      },
      {
        "synchronise": [
          null,
          "displayBalance_2"
        ],
        "result": "displayBalance_2"
      },
      {
        "synchronise": [
          null,
          "press_OK_2"
        ],
        "result": "press_OK_2"
      },
      {
        "synchronise": [
          null,
          "quickWithdrawal_2"
        ],
        "result": "quickWithdrawal_2"
      },
      {
        "synchronise": [
          null,
          "restart_2"
        ],
        "result": "restart_2"
      },
      {
        "synchronise": [
          null,
          "correctAmount_2"
        ],
        "result": "correctAmount_2"
      },
      {
        "synchronise": [
          null,
          "correctPassword_2"
        ],
        "result": "correctPassword_2"
      },
      {
        "synchronise": [
          null,
          "press_finish_2"
        ],
        "result": "press_finish_2"
      },
      {
        "synchronise": [
          null,
          "incorrectAmount_2"
        ],
        "result": "incorrectAmount_2"
      },
      {
        "synchronise": [
          null,
          "incorrectPassword_2"
        ],
        "result": "incorrectPassword_2"
      },
      {
        "synchronise": [
          null,
          "normalWithdrawal_2"
        ],
        "result": "normalWithdrawal_2"
      },
      {
        "synchronise": [
          null,
          "take_cash_2"
        ],
        "result": "take_cash_2"
      }
    ]
  }
}