Commands
This section covers the main process specification and composition commands.
It is worth noting that the result of these commands is of type Composer.Response, which is defined as follows:
1module Response :
2 sig
3 type t =
4 | Ping of float
5 | Create of Process.t
6 | Compose of Process.t * Action.t * Actionstate.t
7 | Verify of Process.t
8 | Deploy of string * (string * string * bool) list
9 | Failed of string
10 | Exception of string
11 (*...*)
12 end
Upon failure a Failed or an Exception response will be issued with an associated message describing the failure. Otherwise, one of the other responses will be returned, as explained in the normal operation of each command below.
create
The create command constructs a new atomic process given the types of its desired inputs and output.
It takes 3 arguments:
string: The name of the process.term list: The list of types of its inputs.term: The type of its output.
All terms are expected to be resources involving HOL Light propositions and the operators ++ and ** operators. No negative operators (NEG, &, %) should be used, including in the input types.
The command returns a Create response with the specification of the created process.
Notes
- Terms in HOL Light must be surrounded by back-ticks
`. - If a process with the same name already exists, a warning will be shown and the old process will be replaced.
- All the elements of the process other than its name and its types, including channel names, π-calculus specification, and provenance are constructed automatically.
Example
The following invocation of create constructs a process named "P" with two inputs of types X and Y++Z respectively and an output of type A**B**C:
1create "P" [`X`; `Y ++ Z`] `A ** B ** C`;;
1Console.Composer.Response.Create
2 {Console.Composer.Process.name = "P";
3 inputs = [(`X`, `cP_X_1`); (`Y ++ Z`, `cP_lB_Y_Plus_Z_rB_2`)];
4 output = (`A ** B ** C`, `oP_lB_A_x_lB_B_x_C_rB_rB_`);
5 prov =
6 Provnode ("times", Provleaf "P",
7 Provnode ("times", Provleaf "P", Provleaf "P"));
8 proc =
9 `P (cP_X_1,cP_lB_Y_Plus_Z_rB_2,oP_lB_A_x_lB_B_x_C_rB_rB_) =
10 Comp (In cP_X_1 [cP_X_1__a_X] Zero)
11 (Comp
12 (Res [cP_lB_Y_Plus_Z_rB_2__opt_Y; cP_lB_Y_Plus_Z_rB_2__opt_Z]
13 (Out cP_lB_Y_Plus_Z_rB_2
14 [cP_lB_Y_Plus_Z_rB_2__opt_Y; cP_lB_Y_Plus_Z_rB_2__opt_Z]
15 (Plus
16 (In cP_lB_Y_Plus_Z_rB_2__opt_Y [cP_lB_Y_Plus_Z_rB_2_Y]
17 (In cP_lB_Y_Plus_Z_rB_2_Y [cP_lB_Y_Plus_Z_rB_2_l_a_Y] Zero))
18 (In cP_lB_Y_Plus_Z_rB_2__opt_Z [cP_lB_Y_Plus_Z_rB_2_Z]
19 (In cP_lB_Y_Plus_Z_rB_2_Z [cP_lB_Y_Plus_Z_rB_2_r_a_Z] Zero)))))
20 (Res
21 [oP_lB_A_x_lB_B_x_C_rB_rB__A; oP_lB_A_x_lB_B_x_C_rB_rB__lB_B_x_C_rB]
22 (Out oP_lB_A_x_lB_B_x_C_rB_rB_
23 [oP_lB_A_x_lB_B_x_C_rB_rB__A; oP_lB_A_x_lB_B_x_C_rB_rB__lB_B_x_C_rB]
24 (Comp
25 (Res [oP_lB_A_x_lB_B_x_C_rB_rB__l_a_A]
26 (Out oP_lB_A_x_lB_B_x_C_rB_rB__A [oP_lB_A_x_lB_B_x_C_rB_rB__l_a_A]
27 Zero))
28 (Res [oP_lB_A_x_lB_B_x_C_rB_rB__rB; oP_lB_A_x_lB_B_x_C_rB_rB__rC]
29 (Out oP_lB_A_x_lB_B_x_C_rB_rB__lB_B_x_C_rB
30 [oP_lB_A_x_lB_B_x_C_rB_rB__rB; oP_lB_A_x_lB_B_x_C_rB_rB__rC]
31 (Comp
32 (Res [oP_lB_A_x_lB_B_x_C_rB_rB__rl_a_B]
33 (Out oP_lB_A_x_lB_B_x_C_rB_rB__rB [oP_lB_A_x_lB_B_x_C_rB_rB__rl_a_B]
34 Zero))
35 (Res [oP_lB_A_x_lB_B_x_C_rB_rB__rr_a_C]
36 (Out oP_lB_A_x_lB_B_x_C_rB_rB__rC [oP_lB_A_x_lB_B_x_C_rB_rB__rr_a_C]
37 Zero)))))))))`;
38 actions = []; copier = false; intermediate = false}
tensor
The tensor command composes two processes in parallel with the TENSOR action.
It takes 2 arguments:
string: The name of the first process to compose.string: The name of the second process to compose.
The command returns a Compose response with the specification of the created intermediate composition, the composition action that was applied, and the resulting actionstate with additional metadata.
Notes
- The name of the resulting intermediate composition is automatically determined using the
"_Step"prefix and an internal step counter.
Example
The following invocation of tensor performs the parallel composition _Step0 of a process P with input X and output A ++ B and a process Q with inputs Y and Z and output C:
1create "P" [`X`] `A ++ B` ;;
2create "Q" [`Y`; `Z`] `C` ;;
3tensor "P" "Q" ;;
1Console.Composer.Response.Compose
2 ({Console.Composer.Process.name = "_Step0";
3 inputs = [(`X`, `cP_X_1`); (`Y`, `cQ_Y_1`); (`Z`, `cQ_Z_2`)];
4 output = (`(A ++ B) ** C`, `c_Step0___Step0__z1`);
5 prov =
6 Provnode ("times", Provnode ("plus", Provleaf "P", Provleaf "P"),
7 Provleaf "Q");
8 proc =
9 `_Step0 (cP_X_1,cQ_Y_1,cQ_Z_2,c_Step0___Step0__z1) =
10 PiTimesProc (A ++ B) C c_Step0___Step0__z1 oP_lB_A_Plus_B_rB_ oQ_C_
11 (P (cP_X_1,oP_lB_A_Plus_B_rB_))
12 (Q (cQ_Y_1,cQ_Z_2,oQ_C_))`;
13 actions =
14 [{Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = "";
15 res = "_Step0"}];
16 copier = false; intermediate = true},
17 {Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = "";
18 res = "_Step0"},
19 {Actionstate.label = "_Step0"; ctr = 0;
20 metas =
21 [`c_Step0___Step0__z1`; `c_Step0___Step0__y1`; `c_Step0___Step0__Q1`;
22 `cQ_Y_1`; `cQ_Z_2`; `oQ_C_`; `cP_X_1`; `oP_lB_A_Plus_B_rB_`];
23 merged = []; iprov = [];
24 prov =
25 [("_Step0",
26 Provnode ("times", Provnode ("plus", Provleaf "P", Provleaf "P"),
27 Provleaf "Q"));
28 ("P", Provnode ("plus", Provleaf "P", Provleaf "P"));
29 ("Q", Provleaf "Q")]})
cwith
The cwith command composes two processes conditionally with the WITH action.
It takes 4 arguments:
string: The name of the first process to compose.string: The type of the input to use from the first process.string: The name of the second process to compose.string: The type of the input to use from the second process.
The command returns a Compose response with the specification of the created intermediate composition, the composition action that was applied, and the resulting actionstate with additional metadata.
Notes
- The name of the resulting intermediate composition is automatically determined using the
"_Step"prefix and an internal step counter. - The types of the selected inputs need to be provided as strings and not as terms.
Example
The following invocation of cwith performs the conditional composition _Step0 of a process P with input X and output A ++ B and a process Q with inputs Y and Z and output C with inputs X and Y selected:
1create "P" [`X`] `A ++ B` ;;
2create "Q" [`Y`; `Z`] `C` ;;
3cwith "P" "X" "Q" "Y" ;;
1Console.Composer.Response.Compose
2 ({Console.Composer.Process.name = "_Step0";
3 inputs = [(`Z`, `cQ_Z_2`); (`X ++ Y`, `c_Step0___Step0__x3`)];
4 output = (`((A ++ B) ** Z) ++ C`, `c_Step0___Step0__y3`);
5 prov =
6 Provnode ("plus",
7 Provnode ("times",
8 Provnode ("plus", Provleaf "&_Step0", Provleaf "&_Step0"),
9 Provleaf "&_Step0"),
10 Provleaf "&_Step0");
11 proc =
12 `_Step0 (cQ_Z_2,c_Step0___Step0__x3,c_Step0___Step0__y3) =
13 PiWithProc (NEG X) (NEG Y) c_Step0___Step0__x3 cP_X_1 cQ_Y_1
14 c_Step0___Step0__uI3
15 c_Step0___Step0__vI3
16 (PiPlusLProc ((A ++ B) ** Z) C c_Step0___Step0__y3 c_Step0___Step0__z1
17 c_Step0___Step0__uR3
18 c_Step0___Step0__vR3
19 (PiTimesProc (A ++ B) Z c_Step0___Step0__z1 oP_lB_A_Plus_B_rB_
20 c_Step0___Step0__y1
21 (P (cP_X_1,oP_lB_A_Plus_B_rB_))
22 (PiIdProc Z cQ_Z_2 c_Step0___Step0__y1 c_Step0___Step0__m2)))
23 (PiPlusRProc ((A ++ B) ** Z) C c_Step0___Step0__y3 oQ_C_
24 c_Step0___Step0__uE3
25 c_Step0___Step0__vE3
26 (Q (cQ_Y_1,cQ_Z_2,oQ_C_)))`;
27 actions =
28 [{Action.act = "WITH"; larg = "P"; lsel = "X"; rarg = "Q"; rsel = "Y";
29 res = "_Step0"}];
30 copier = false; intermediate = true},
31 {Action.act = "WITH"; larg = "P"; lsel = "X"; rarg = "Q"; rsel = "Y";
32 res = "_Step0"},
33 {Actionstate.label = "_Step0"; ctr = 0;
34 metas =
35 [`c_Step0___Step0__x3`; `c_Step0___Step0__uI3`; `c_Step0___Step0__vI3`;
36 `c_Step0___Step0__uR3`; `c_Step0___Step0__vR3`; `c_Step0___Step0__y3`;
37 `c_Step0___Step0__d3`; `c_Step0___Step0__uE3`; `c_Step0___Step0__vE3`;
38 `c_Step0___Step0__Q3`; `c_Step0___Step0__m2`; `c_Step0___Step0__z1`;
39 `c_Step0___Step0__y1`; `c_Step0___Step0__Q1`; `cQ_Y_1`; `cQ_Z_2`;
40 `oQ_C_`; `cP_X_1`; `oP_lB_A_Plus_B_rB_`];
41 merged = [(`NEG (X ++ Y) <> c_Step0___Step0__x3`, "cP_X_1", "cQ_Y_1")];
42 iprov = [];
43 prov =
44 [("_Step0",
45 Provnode ("plus",
46 Provnode ("times",
47 Provnode ("plus", Provleaf "&_Step0", Provleaf "&_Step0"),
48 Provleaf "&_Step0"),
49 Provleaf "&_Step0"));
50 ("P", Provnode ("plus", Provleaf "P", Provleaf "P"));
51 ("Q", Provleaf "Q")]})
join
The join command composes two processes in sequence with the JOIN action.
It takes 4 arguments:
string: The name of the first process to compose.string: The path to a sub-term of the output of the first process.string: The name of the second process to compose.string: The type of the input to use from the second process.
The command returns a Compose response with the specification of the created intermediate composition, the composition action that was applied, and the resulting actionstate with additional metadata.
Notes
- The name of the resulting intermediate composition is automatically determined using the
"_Step"prefix and an internal step counter. - The path to a sub-type of the output of the first process must follow the syntax of HOL Light's
find_pathfunction. - The types of the selected input need to be provided as a string and not as a term.
Example
The following invocation of join performs the sequential composition _Step0 of a process P with input X and output A ++ B and a process Q with inputs A and Y and output C:
1create "P" [`X`] `A ++ B` ;;
2create "Q" [`A`; `Z`] `C` ;;
3join "P" "lr" "Q" "A" ;;
1Console.Composer.Response.Compose
2 ({Console.Composer.Process.name = "_Step0";
3 inputs = [(`X`, `cP_X_1`); (`Z`, `cQ_Z_2`)];
4 output = (`C ++ (Z ** B)`, `c_Step0___Step0__y3`);
5 prov =
6 Provnode ("plus", Provleaf "Q",
7 Provnode ("times", Provleaf "Q:cQ_Z_2", Provleaf "P"));
8 proc =
9 `_Step0 (cP_X_1,cQ_Z_2,c_Step0___Step0__y3) =
10 PiCutProc (A ++ B) c_Step0___Step0__z7 c_Step0___Step0__x3
11 oP_lB_A_Plus_B_rB_
12 (PiWithProc (NEG A) (NEG B) c_Step0___Step0__x3 cQ_A_1
13 c_Step0___Step0__c3
14 c_Step0___Step0__uI3
15 c_Step0___Step0__vI3
16 (PiPlusLProc C (Z ** B) c_Step0___Step0__y3 oQ_C_
17 c_Step0___Step0__uR3
18 c_Step0___Step0__vR3
19 (Q (cQ_A_1,cQ_Z_2,oQ_C_)))
20 (PiPlusRProc C (Z ** B) c_Step0___Step0__y3 c_Step0___Step0__d3
21 c_Step0___Step0__uE3
22 c_Step0___Step0__vE3
23 (PiTimesProc Z B c_Step0___Step0__d3 c_Step0___Step0__x4
24 c_Step0___Step0__y4
25 (PiIdProc Z cQ_Z_2 c_Step0___Step0__x4 c_Step0___Step0__m5)
26 (PiIdProc B c_Step0___Step0__c3 c_Step0___Step0__y4
27 c_Step0___Step0__m6))))
28 (P (cP_X_1,oP_lB_A_Plus_B_rB_))`;
29 actions =
30 [{Action.act = "JOIN"; larg = "P"; lsel = "lr"; rarg = "Q"; rsel = "A";
31 res = "_Step0"}];
32 copier = false; intermediate = true},
33 {Action.act = "JOIN"; larg = "P"; lsel = "lr"; rarg = "Q"; rsel = "A";
34 res = "_Step0"},
35 {Actionstate.label = "_Step0"; ctr = 0;
36 metas =
37 [`c_Step0___Step0__z7`; `c_Step0___Step0__y7`; `c_Step0___Step0__Q7`;
38 `c_Step0___Step0__m6`; `c_Step0___Step0__m5`; `c_Step0___Step0__x4`;
39 `c_Step0___Step0__y4`; `c_Step0___Step0__P4`; `c_Step0___Step0__Q4`;
40 `c_Step0___Step0__x3`; `c_Step0___Step0__c3`; `c_Step0___Step0__uI3`;
41 `c_Step0___Step0__vI3`; `c_Step0___Step0__uR3`; `c_Step0___Step0__vR3`;
42 `c_Step0___Step0__y3`; `c_Step0___Step0__d3`; `c_Step0___Step0__uE3`;
43 `c_Step0___Step0__vE3`; `c_Step0___Step0__Q3`; `cQ_A_1`; `cQ_Z_2`;
44 `oQ_C_`; `cP_X_1`; `oP_lB_A_Plus_B_rB_`];
45 merged = [];
46 iprov =
47 [(`A ++ B`, Provnode ("plus", Provleaf "cQ_A_1:1", Provleaf "#"))];
48 prov =
49 [("Q", Provleaf "Q");
50 ("_Step0",
51 Provnode ("plus", Provleaf "Q",
52 Provnode ("times", Provleaf "Q:cQ_Z_2", Provleaf "P")));
53 ("P", Provnode ("plus", Provleaf "P", Provleaf "P"))]})
compose1
The compose1 command composes two processes with an explicit composition action.
It takes 1 argument:
Action.t: The composition action to perform.
This command is intended for advanced usage, for instance with a custom action, or some other action parameter not handled by the other commands.
The command returns a Compose response with the specification of the created intermediate composition, the composition action that was applied, and the resulting actionstate with additional metadata.
Notes
- If an intermediate composition with the same name as the action's result already exists, a warning will be shown and the old process will be replaced.
Example
The following invocation of compose1 performs the parallel composition R of a process P with input X and output A ++ B and a process Q with inputs Y and Z and output C:
1create "P" [`X`] `A ++ B` ;;
2create "Q" [`Y`; `Z`] `C` ;;
3compose1 {Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = ""; res = "R"} ;;
1Console.Composer.Response.Compose
2 ({Console.Composer.Process.name = "R";
3 inputs = [(`X`, `cP_X_1`); (`Y`, `cQ_Y_1`); (`Z`, `cQ_Z_2`)];
4 output = (`(A ++ B) ** C`, `cR__R__z1`);
5 prov =
6 Provnode ("times", Provnode ("plus", Provleaf "P", Provleaf "P"),
7 Provleaf "Q");
8 proc =
9 `R (cP_X_1,cQ_Y_1,cQ_Z_2,cR__R__z1) =
10 PiTimesProc (A ++ B) C cR__R__z1 oP_lB_A_Plus_B_rB_ oQ_C_
11 (P (cP_X_1,oP_lB_A_Plus_B_rB_))
12 (Q (cQ_Y_1,cQ_Z_2,oQ_C_))`;
13 actions =
14 [{Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = "";
15 res = "R"}];
16 copier = false; intermediate = true},
17 {Action.act = "TENSOR"; larg = "P"; lsel = ""; rarg = "Q"; rsel = "";
18 res = "R"},
19 {Actionstate.label = "R"; ctr = 0;
20 metas =
21 [`cR__R__z1`; `cR__R__y1`; `cR__R__Q1`; `cQ_Y_1`; `cQ_Z_2`; `oQ_C_`;
22 `cP_X_1`; `oP_lB_A_Plus_B_rB_`];
23 merged = []; iprov = [];
24 prov =
25 [("R",
26 Provnode ("times", Provnode ("plus", Provleaf "P", Provleaf "P"),
27 Provleaf "Q"));
28 ("P", Provnode ("plus", Provleaf "P", Provleaf "P"));
29 ("Q", Provleaf "Q")]})