BigraphER

More information about BigraphER can be found on the following websites:

Exporting a `PureReactiveSystem`

The following example specifies a bigraphical actor-based system and shows how to convert it into BigraphER specification file format. The system's specification follows the *.big model file presented here.

caution

When converting bigraph instance models into the .big model file (conforming to the BigraphER specification language), some ambiguous cases may occur that require manual treatment.

For some instances, Bigraph Framework has no information whether to "finalize" the leaves of a hierarchy with a barren, i.e., using the expression ".1". Bigraphs modelled within Bigraph Framework do not need this information, as the bigraph itself is represented as a graphical structure and not an algebraic expression as it is the case with the BigraphER specification language.

To circumvent this problem, the encoding algorithm attaches ".1" automatically to every control that is not atomic and has no sites specified. Vice versa, if a site is required under a node, it must be explicitly modelled within Bigraph Framework as it cannot be inferred automatically. This applies to all bigraph and predicate variable expression of the BigraphER specification language. For rule declarations, we do not follow this strategy, i.e., the expression ".1" is not attached at all. Therefore, the rule needs to be possibly manually edited afterwards. Using the instantiation map is advised to clearly express control duplications or deletions.

The signature:

import static org.bigraphs.framework.core.factory.BigraphFactory.*;

private static DefaultDynamicSignature createSignature() { 
	DynamicSignatureBuilder defaultBuilder = pureSignatureBuilder();
	defaultBuilder.newControl("A", 1).assign().newControl("A'", 1).assign().newControl("Mail", 0).assign().newControl("M", 2).status(ControlStatus.ATOMIC).assign().newControl("Snd", 0).assign().newControl("Ready", 0).assign().newControl("New", 0).assign().newControl("Fun", 0).assign();
}

Next, we need to specify the agent:

import static org.bigraphs.framework.core.factory.BigraphFactory.*;

public void bigrapher_test01() throws InvalidConnectionException, TypeNotExistsException, InvalidReactionRuleException, IOException { 
	DefaultDynamicSignature sig = createSignature();
	createOrGetBigraphMetaModel(sig);
	PureBigraphBuilder<DefaultDynamicSignature> builder = pureBuilder(sig);
	PureBigraph s0 = builder.createRoot().addChild("A", "a").down().addChild("Snd").down().addChild("M", "a").linkToOuter("v_a").addChild("Ready").down().addChild("Fun").top().addChild("A", "b").down().addChild("Snd").down().addChild("M", "a").linkToOuter("v_b").top().addChild("Mail").createBigraph();
}

Then, followed by the rules:

public void bigrapher_test01() throws InvalidConnectionException, TypeNotExistsException, InvalidReactionRuleException, IOException { 
	// ...
	PureBigraph sndRedex = builder.spawnNewOne().createRoot().addChild("A", "a0").down().addChild("Snd").down().addChild("M", "a1").linkToOuter("v").addSite().top().addChild("Mail").createBigraph();
	PureBigraph sndReactum = builder.spawnNewOne().createRoot().addChild("A", "a0").addChild("Mail").down().addChild("M", "a1").linkToOuter("v").addSite().createBigraph();
	ParametricReactionRule<PureBigraph> snd = new ParametricReactionRule<>(sndRedex, sndReactum).withLabel("snd");
	PureBigraph readyRedex = builder.spawnNewOne().createRoot().addChild("A", "a").down().addChild("Ready").up().addChild("Mail").down().addChild("M", "a").linkToOuter("v").addSite().createBigraph();
	PureBigraphBuilder<DefaultDynamicSignature> readyBuilder = builder.spawnNewOne();
	readyBuilder.createOuterName("v");
	PureBigraph readyReactum = readyBuilder.createRoot().addChild("A", "a").addChild("Mail").createBigraph();
	ParametricReactionRule<PureBigraph> ready = new ParametricReactionRule<>(readyRedex, readyReactum).withLabel("ready");
	PureBigraph lambdaRedex = builder.spawnNewOne().createRoot().addChild("A", "a").down().addChild("Fun").createBigraph();
	PureBigraph lambdaReactum = builder.spawnNewOne().createRoot().addChild("A", "a").createBigraph();
	ParametricReactionRule<PureBigraph> lambda = new ParametricReactionRule<>(lambdaRedex, lambdaReactum).withLabel("lambda");
	PureBigraph newRedex = builder.spawnNewOne().createRoot().addChild("A", "a0").down().addChild("New").down().addChild("A'", "a1").down().addSite().up().addSite().up().addSite().createBigraph();
	PureBigraph newReactum = builder.spawnNewOne().createRoot().addChild("A", "a0").down().addSite().addSite().up().addChild("A", "a1").down().addSite().addSite().createBigraph();
	InstantiationMap instMap = InstantiationMap.create(newReactum.getSites().size()).map(0, 1).map(1, 2).map(2, 0).map(3, 2);
	ParametricReactionRule<PureBigraph> newRR = new ParametricReactionRule<>(newRedex, newReactum, instMap).withLabel("new");
}

Note how we attach a label to the rules. This allows the converter later to use these labels as new variable names for the *.big model file

The predicate:

public void bigrapher_test01() throws InvalidConnectionException, TypeNotExistsException, InvalidReactionRuleException, IOException { 
	// ...
	ReactiveSystemPredicate<PureBigraph> phi = SubBigraphMatchPredicate.create(builder.spawnNewOne().createRoot().addChild("Mail").down().addChild("M", "a").linkToOuter("v").addSite().top().createBigraph()).withLabel("phi");
}

Now, since everything is defined, we need to create a reactive system and add the agent, rules, and the predicate:

public void bigrapher_test01() throws InvalidConnectionException, TypeNotExistsException, InvalidReactionRuleException, IOException { 
	// ...
	PureReactiveSystem rs = new PureReactiveSystem();
	rs.setAgent(s0);
	rs.addReactionRule(snd);
	rs.addReactionRule(ready);
	rs.addReactionRule(lambda);
	rs.addReactionRule(newRR);
	rs.addPredicate(phi);
	BigrapherTransformator transformator = new BigrapherTransformator();
	transformator.toOutputStream(rs, System.out);
}

The transformator will produce the output as shown below:

ctrl A = 1;
ctrl A' = 1;
ctrl Mail = 0;
atomic ctrl M = 2;
ctrl Snd = 0;
ctrl Ready = 0;
ctrl New = 0;
ctrl Fun = 0;

react snd = (A{a0}.Snd.( M{a1, v} | id(1) ) | Mail) --> (A{a0} | Mail.( id(1) | M{a1, v} ));
react ready = (A{a}.Ready | Mail.( M{a, v} | id(1) )) --> (A{a} | Mail) | {v};
react lambda = (A{a}.Fun) --> (A{a});
react new = (A{a0}.( id(1) | New.( id(1) | A'{a1}.id(1) ) )) --> (A{a1}.( id(1) | id(1) ) | A{a0}.( id(1) | id(1) )) @ [1, 2, 0, 2];

big bigraphbasemodel = Mail.1 | A{b}.Snd.M{a, v_b} | A{a}.Snd.( M{a, v_a} | Ready.Fun.1 ) ;

big phi = Mail.( M{a, v} | id(1) );

begin brs
    init bigraphbasemodel;
    rules = [{snd,ready,lambda,new}];
    preds = {phi};
end

The user can verify that the output, or more specifically the behaviour of the system, resembles the one provided here:

$ bigrapher full -v -s ./states -t trans.svg -f svg,json -M 20 actors.big

Note that a folder called states must exist next to the model file actors.big.

Exporting a PureReactiveSystem​

caution

Exporting a `PureReactiveSystem`