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)
)
);