/* This script show a very simple example of 4 components: - a choreography "spec" with two roles: requestor (a) and responder (b) - two local specifications: "client" & "seller" - a component "impl" is a composition of "client" and "seller" */ //Declare components here. They respect either DOT language or ChorD language. DECLARATIONS component spec STG // list of states. The first state is initial of STG 1; 2; 3; // list of transitions 1 -> 2 [label="request[a,b].<x>"]; //a bound interaction 2 -> 3 [label="[x>0] response[b,a]."]; //an interaction without data 2 -> 3 [label ="[x<=0] error[b,a]."]; end component component client STG 1; 2; 3; 1 -> 2 [label="request[a,b]!<x1>"]; 2 -> 3 [label="response[b,a]?"]; end component component seller chorD request[a,b]?<y1> ; response[b,a]! end component //the "impl" is the composition of "client" and "seller" component impl chorD client || seller end component //MUTATION //we change variables in spec & impl to free-variables //==> they are free-variables at init states ==> they can be configured before runtime //==> conformance depends on their initial values ==> inconclusive component spec1 STG // list of states. The first state is initial of STG 1; 2; 3; // list of transitions 1 -> 2 [label="request[a,b].x"]; //a bound interaction 2 -> 3 [label="[x>0] response[b,a]."]; //an interaction without data 2 -> 3 [label ="[x<=0] error[b,a]."]; end component component impl1 STG 1; 2; 3; 1 -> 2 [label="request[a,b].x1"]; 2 -> 3 [label="response[b,a]."]; end component //List of commands COMMANDS //display STG graphics of components showSTG spec client seller impl //check if the implementation "impl" conforms to the specification "spec" conformance impl spec showSTG spec1 impl1 conformance impl1 spec1 //project "spec" on it local roles to obtain local models projection spec SYNC //synchronous communication mode, the other modes: ASYNC_SENDER, ASYNC_RECEIVER and ASYNC_DISJOINT
  • Output
  • Expand