{
  "transform": {
    "system": "// Place template instantiations here.\n//Process = Template();\n// List one or more processes to be composed into a system.\nsystem env1, env2, sut;",
    "queries": {
      "query": [
        {
          "formula": "A[] P.id1 --> P.id5",
          "comment": ""
        },
        {
          "formula": "deadlock",
          "comment": ""
        }
      ]
    },
    "declarations": [
      {
        "type": "channel",
        "name": "ch"
      },
      {
        "type": "channel",
        "name": "i_ch"
      },
      {
        "type": "channel",
        "name": "o_ch"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i1",
        "value": "1"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i2",
        "value": "2"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i3",
        "value": "3"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i4",
        "value": "4"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i5",
        "value": "5"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i6",
        "value": "6"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i7",
        "value": "7"
      },
      {
        "constant": true,
        "type": "number",
        "name": "i8",
        "value": "8"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o1",
        "value": "1"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o2",
        "value": "2"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o3",
        "value": "3"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o4",
        "value": "4"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o5",
        "value": "5"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o6",
        "value": "6"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o7",
        "value": "7"
      },
      {
        "constant": true,
        "type": "number",
        "name": "o8",
        "value": "8"
      },
      {
        "constant": false,
        "type": "array",
        "name": "t",
        "length": 8,
        "elementType": "boolean",
        "value": [
          "0",
          "0",
          "0",
          "0",
          "0",
          "0",
          "0",
          "0"
        ]
      },
      {
        "constant": false,
        "type": "number",
        "name": "inp",
        "value": "5"
      },
      {
        "constant": false,
        "type": "number",
        "name": "out",
        "value": "5"
      },
      {
        "constant": false,
        "type": "number",
        "name": "i_ch_var"
      },
      {
        "constant": false,
        "type": "number",
        "name": "o_ch_var"
      },
      {
        "constant": false,
        "type": "clock",
        "name": "cl"
      },
      {
        "constant": false,
        "type": "boolean",
        "name": "v",
        "value": "0"
      }
    ],
    "templates": [
      {
        "name": {
          "text": "sut",
          "x": 5,
          "y": 5
        },
        "rootNode": "id0",
        "declarations": [],
        "nodes": [
          {
            "id": "id0",
            "x": -204,
            "y": -102,
            "name": {
              "text": "id0",
              "x": -246,
              "y": -119
            }
          },
          {
            "id": "id1",
            "x": -68,
            "y": -230,
            "name": {
              "text": "id1",
              "x": -102,
              "y": -238
            }
          },
          {
            "id": "id2",
            "x": 59,
            "y": -102,
            "name": {
              "text": "id3",
              "x": 76,
              "y": -119
            }
          },
          {
            "id": "id3",
            "x": -68,
            "y": 42,
            "name": {
              "text": "id2",
              "x": -102,
              "y": 42
            },
            "invariant": {
              "x": -76,
              "y": 59,
              "text": "cl<=15"
            }
          }
        ],
        "transitions": [
          {
            "source": "id2",
            "target": "id3",
            "synchronisation": {
              "x": 8,
              "y": -26,
              "text": "i_ch?"
            },
            "assignment": {
              "x": -8,
              "y": -9,
              "text": "out=o2"
            },
            "comments": {
              "x": 34,
              "y": -51,
              "text": "trans6"
            }
          },
          {
            "source": "id3",
            "target": "id1",
            "guard": {
              "x": 153,
              "y": -170,
              "text": "i_ch_var>=i2 && \ni_ch_var<=6"
            },
            "assignment": {
              "x": 153,
              "y": -128,
              "text": "out=o5"
            },
            "comments": {
              "x": 153,
              "y": -204,
              "text": "trans7"
            }
          },
          {
            "source": "id1",
            "target": "id2",
            "synchronisation": {
              "x": 8,
              "y": -179,
              "text": "o_ch!"
            },
            "assignment": {
              "x": 25,
              "y": -162,
              "text": "o_ch_var=out,\n   cl=0"
            },
            "comments": {
              "x": -8,
              "y": -196,
              "text": "trans5"
            }
          },
          {
            "source": "id1",
            "target": "id0",
            "synchronisation": {
              "x": -221,
              "y": -179,
              "text": "o_ch!"
            },
            "assignment": {
              "x": -272,
              "y": -161,
              "text": "o_ch_var=out,\ncl=0"
            },
            "comments": {
              "x": -204,
              "y": -204,
              "text": "trans3"
            }
          },
          {
            "source": "id0",
            "target": "id3",
            "guard": {
              "x": -119,
              "y": -34,
              "text": "i_ch_var<=i5"
            },
            "synchronisation": {
              "x": -136,
              "y": -51,
              "text": "i_ch?"
            },
            "assignment": {
              "x": -102,
              "y": -17,
              "text": "out=o1"
            },
            "comments": {
              "x": -144,
              "y": -68,
              "text": "trans2"
            }
          },
          {
            "source": "id3",
            "target": "id0",
            "synchronisation": {
              "x": -212,
              "y": -1,
              "text": "o_ch!"
            },
            "assignment": {
              "x": -212,
              "y": 16,
              "text": "o_ch_var=out,\ncl=0"
            },
            "comments": {
              "x": -212,
              "y": -17,
              "text": "trans4"
            }
          },
          {
            "source": "id1",
            "target": "id1",
            "assignment": {
              "x": -93,
              "y": -289,
              "text": "out=o3"
            },
            "comments": {
              "x": -93,
              "y": -315,
              "text": "trans8"
            }
          },
          {
            "source": "id0",
            "target": "id1",
            "guard": {
              "x": -153,
              "y": -128,
              "text": "i_ch_var>5"
            },
            "synchronisation": {
              "x": -136,
              "y": -145,
              "text": "i_ch?"
            },
            "assignment": {
              "x": -153,
              "y": -111,
              "text": "out=o6"
            },
            "comments": {
              "x": -102,
              "y": -170,
              "text": "trans1"
            }
          }
        ]
      },
      {
        "name": {},
        "rootNode": "id4",
        "declarations": [],
        "nodes": [
          {
            "id": "id4",
            "x": 0,
            "y": 0,
            "name": {
              "text": "id30",
              "x": -51,
              "y": -8
            }
          },
          {
            "id": "id5",
            "x": 136,
            "y": 0,
            "name": {
              "text": "id31",
              "x": 153,
              "y": -8
            }
          }
        ],
        "transitions": [
          {
            "source": "id4",
            "target": "id5",
            "synchronisation": {
              "x": 85,
              "y": -34,
              "text": "ch?"
            },
            "assignment": {
              "x": 85,
              "y": -17,
              "text": "v=1"
            },
            "comments": {
              "x": 17,
              "y": -25,
              "text": "trans13"
            }
          },
          {
            "source": "id5",
            "target": "id4",
            "assignment": {
              "x": 85,
              "y": 25,
              "text": "inp=i7"
            },
            "testcode": {
              "text": "trans"
            },
            "comments": {
              "x": 17,
              "y": 17,
              "text": "trans15"
            }
          },
          {
            "source": "id5",
            "target": "id4",
            "assignment": {
              "x": 85,
              "y": -68,
              "text": "inp=i2"
            },
            "comments": {
              "x": 17,
              "y": -68,
              "text": "trans14"
            }
          }
        ]
      },
      {
        "name": {},
        "rootNode": "id6",
        "declarations": [],
        "nodes": [
          {
            "id": "id6",
            "x": -748,
            "y": -357,
            "name": {
              "text": "id20",
              "x": -799,
              "y": -383
            },
            "invariant": {
              "x": -807,
              "y": -366,
              "text": "cl<=20"
            }
          },
          {
            "id": "id7",
            "x": -578,
            "y": -357,
            "name": {
              "text": "id21",
              "x": -561,
              "y": -366
            }
          }
        ],
        "transitions": [
          {
            "source": "id6",
            "target": "id6",
            "guard": {
              "x": -799,
              "y": -451,
              "text": "out>5&&v==0"
            },
            "synchronisation": {
              "x": -773,
              "y": -476,
              "text": "ch!"
            },
            "assignment": {
              "x": -764,
              "y": -425,
              "text": "cl=0"
            },
            "comments": {
              "x": -841,
              "y": -417,
              "text": "trans9"
            }
          },
          {
            "source": "id6",
            "target": "id7",
            "guard": {
              "x": -688,
              "y": -417,
              "text": "v==1"
            },
            "synchronisation": {
              "x": -688,
              "y": -434,
              "text": "i_ch!"
            },
            "assignment": {
              "x": -688,
              "y": -400,
              "text": "i_ch_var=inp"
            },
            "comments": {
              "x": -688,
              "y": -451,
              "text": "trans11"
            }
          },
          {
            "source": "id7",
            "target": "id6",
            "synchronisation": {
              "x": -688,
              "y": -332,
              "text": "o_ch?"
            },
            "assignment": {
              "x": -688,
              "y": -315,
              "text": "out=o_ch_var,\ncl=0"
            },
            "comments": {
              "x": -688,
              "y": -357,
              "text": "trans12"
            }
          },
          {
            "source": "id6",
            "target": "id6",
            "guard": {
              "x": -799,
              "y": -281,
              "text": "out<=5&&v==0"
            },
            "synchronisation": {
              "x": -765,
              "y": -298,
              "text": "ch!"
            },
            "assignment": {
              "x": -765,
              "y": -264,
              "text": "cl=0"
            },
            "comments": {
              "x": -841,
              "y": -315,
              "text": "trans10"
            }
          }
        ]
      }
    ]
  }
}