Reaction Systems Specification Language

Here is an example of how to encode the Train-Gate-Controller model as a Distributed Reaction System (with Context Automaton):

options { use-context-automaton; make-progressive; };
reactions {

    train0 {
        {{out}, {} -> {approach}};
        {{approach}, {req} -> {req}};
        {{allowed}, {} -> {in}};
        {{in}, {} -> {out,leave}};
        {{req}, {in} -> {req}};
    };

    train1 {
        {{out}, {} -> {approach}};
        {{approach}, {req} -> {req}};
        {{allowed}, {} -> {in}};
        {{in}, {} -> {out,leave}};
        {{req}, {in} -> {req}};
    };

    train2 {
        {{out}, {} -> {approach}};
        {{approach}, {req} -> {req}};
        {{allowed}, {} -> {in}};
        {{in}, {} -> {out,leave}};
        {{req}, {in} -> {req}};
    };
};

context-automaton {
    states { init, green, red };
    init-state { init };
    transitions {
        { train0={out} train1={out} train2={out} }: init -> green;
        { train0={allowed} }: green -> red : train0.req;
        { train1={allowed} }: green -> red : train1.req;
        { train2={allowed} }: green -> red : train2.req;
        { train0={} }: green -> green : ~train0.req AND ~train1.req AND ~train2.req;
        { train1={} }: green -> green : ~train0.req AND ~train1.req AND ~train2.req;
        { train2={} }: green -> green : ~train0.req AND ~train1.req AND ~train2.req;
        { train0={} }: red -> green : train0.leave;
        { train1={} }: red -> green : train1.leave;
        { train2={} }: red -> green : train2.leave;
        { train0={} }: red -> red : ~train0.leave AND ~train1.leave AND ~train2.leave;
        { train1={} }: red -> red : ~train0.leave AND ~train1.leave AND ~train2.leave;
        { train2={} }: red -> red : ~train0.leave AND ~train1.leave AND ~train2.leave;

    };
};

Properties expressed in rsCTLK can be specified in the following way:

rsctlk-property { f1 : EF( E<train0.allowed>X( train0.in ) ) AND EF( E<train1.allowed>X( train1.in ) ) AND EF( E<train2.allowed>X( train2.in ) ) };

rsctlk-property { f2 : EF( train0.approach AND train1.approach AND train2.approach ) };

rsctlk-property { f3 : AG( train0.in IMPLIES K[train0](~train1.in AND ~train2.in) ) };

rsctlk-property { f4 : AG( train0.in IMPLIES C[train0,train1,train2](~train1.in AND ~train2.in) ) };