{
  "states": [
    "Closed",
    "Listen",
    "Request",
    "Respond",
    "PartOpen",
    "Open",
    "CloseReq",
    "Closing",
    "TimeWait",
    "Stable",
    "Changing",
    "Unstable"
  ],
  "initial_state": "Closed",
  "final_states": [],
  "transitions": [
    {
      "from": "Closed",
      "event": "cond passive_open",
      "action": "transition",
      "to": "Listen"
    },
    {
      "from": "Closed",
      "event": "cond active_open",
      "action": "send DCCP-Request",
      "to": "Request"
    },
    {
      "from": "Closed",
      "event": "send DCCP-Request",
      "action": "set GSS ISS",
      "to": "Request"
    },
    {
      "from": "Listen",
      "event": "recv DCCP-Request",
      "action": "send DCCP-Response",
      "to": "Respond"
    },
    {
      "from": "Request",
      "event": "recv DCCP-Response",
      "action": "send DCCP-Ack",
      "to": "PartOpen"
    },
    {
      "from": "Request",
      "event": "recv DCCP-Sync",
      "action": "send DCCP-Reset",
      "to": "Request"
    },
    {
      "from": "Request",
      "event": "recv Reset",
      "action": "transition",
      "to": "Closed"
    },
    {
      "from": "Respond",
      "event": "send DCCP-Response",
      "action": "transition",
      "to": "Open"
    },
    {
      "from": "Respond",
      "event": "recv Ack",
      "action": "transition",
      "to": "Open"
    },
    {
      "from": "Respond",
      "event": "recv DataAck",
      "action": "transition",
      "to": "Open"
    },
    {
      "from": "Respond",
      "event": "recv Request",
      "action": "send Response",
      "to": "Respond"
    },
    {
      "from": "PartOpen",
      "event": "send DCCP-Ack",
      "action": "transition",
      "to": "Open"
    },
    {
      "from": "PartOpen",
      "event": "recv packet",
      "action": "transition",
      "to": "Open"
    },
    {
      "from": "PartOpen",
      "event": "recv Response",
      "action": "send Ack",
      "to": "PartOpen"
    },
    {
      "from": "Open",
      "event": "cond server_active_close",
      "action": "send CloseReq",
      "to": "CloseReq"
    },
    {
      "from": "Open",
      "event": "cond active_close",
      "action": "send Close",
      "to": "Closing"
    },
    {
      "from": "Open",
      "event": "recv CloseReq",
      "action": "send Close",
      "to": "Closing"
    },
    {
      "from": "Open",
      "event": "recv Close",
      "action": "send Reset",
      "to": "Closed"
    },
    {
      "from": "Open",
      "event": "send DCCP-CloseReq",
      "action": "transition",
      "to": "CloseReq"
    },
    {
      "from": "Open",
      "event": "send DCCP-Close",
      "action": "transition",
      "to": "Closing"
    },
    {
      "from": "Open",
      "event": "recv DCCP-CloseReq",
      "action": "send DCCP-Reset",
      "to": "Closed"
    },
    {
      "from": "Open",
      "event": "recv DCCP-Close",
      "action": "send DCCP-Reset",
      "to": "Closed"
    },
    {
      "from": "Open",
      "event": "recv DCCP-Reset",
      "action": "transition",
      "to": "Closed"
    },
    {
      "from": "Open",
      "event": "recv sequence-invalid",
      "action": "send DCCP-Sync",
      "to": "Open"
    },
    {
      "from": "Open",
      "event": "recv DCCP-Sync",
      "action": "send DCCP-SyncAck",
      "to": "Open"
    },
    {
      "from": "CloseReq",
      "event": "recv Close",
      "action": "send Reset",
      "to": "Closed"
    },
    {
      "from": "CloseReq",
      "event": "recv DCCP-Close",
      "action": "send DCCP-Reset",
      "to": "Closed"
    },
    {
      "from": "Closing",
      "event": "recv Reset",
      "action": "transition",
      "to": "TimeWait"
    },
    {
      "from": "Closing",
      "event": "recv DCCP-Reset",
      "action": "transition",
      "to": "Closed"
    },
    {
      "from": "TimeWait",
      "event": "timeout 2MSL",
      "action": "transition",
      "to": "Closed"
    },
    {
      "from": "Stable",
      "event": "recv Change_R",
      "action": "send Confirm_L",
      "to": "Stable"
    },
    {
      "from": "Stable",
      "event": "cond app_protocol_event",
      "action": "send Change_L",
      "to": "Changing"
    },
    {
      "from": "Changing",
      "event": "recv Confirm_R",
      "action": "set accept_value",
      "to": "Stable"
    },
    {
      "from": "Changing",
      "event": "recv empty_Confirm_R",
      "action": "set revert_to_old_value",
      "to": "Stable"
    },
    {
      "from": "Changing",
      "event": "cond pref_list_changes",
      "action": "transition",
      "to": "Unstable"
    },
    {
      "from": "Changing",
      "event": "timeout",
      "action": "send Change_L",
      "to": "Changing"
    },
    {
      "from": "Changing",
      "event": "recv non_ack",
      "action": "send Change_L",
      "to": "Changing"
    },
    {
      "from": "Unstable",
      "event": "send Change_L",
      "action": "transition",
      "to": "Changing"
    },
    {
      "from": "Unstable",
      "event": "recv Confirm_R",
      "action": "set ignore",
      "to": "Unstable"
    },
    {
      "from": "Unstable",
      "event": "recv Change_R",
      "action": "set ignore",
      "to": "Unstable"
    }
  ]
}