C2PO Language Support

Language support for C2PO; the input language for R2U2. Automatically applies syntax highlighting to file with extension .c2po.

As an example C2PO file:

-- A specification set for a Request-Arbiter system.
STRUCT
    Request: { state: int; time_active: float; };
    Arbiter: { ReqSet: Request[]; };

INPUT
    st0, st1, st2, st3: int;
    ta0, ta1, ta2, ta3: float;

DEFINE
    WAIT := 0; GRANT := 1; REJECT := 2;

    rq0 := Request(st0, ta0); rq1 := Request(st1, ta1); 
    rq2 := Request(st2, ta2); rq3 := Request(st3, ta3); 

    Arb0 := Arbiter({rq0, rq1}); Arb1 := Arbiter({rq2, rq3});
    ArbSet := {Arb0, Arb1};

FTSPEC
    -- The active times for 'rq_0' and 'rq_1' shall differ by no more than 10.0 seconds
    (rq0.time_active - rq1.time_active) < 10.0 &&
    (rq1.time_active - rq0.time_active) < 10.0;

    -- For each request 'r' of each arbiter in 'ArbSet', r's status shall be 'GRANT' or 'REJECT' 
    -- within the next 5 seconds and until then shall be 'WAITING'.
    foreach(arb: ArbSet)(
        foreach(rq: arb.ReqSet)(
            (rq.state == WAIT) U[0,5] (rq.state == GRANT || rq.state == REJECT)
        )
    );