#Signature
ctrl E = 1;
ctrl V = 2;
ctrl I = 0;
ctrl T = 0;
ctrl N = 2;
atomic ctrl P = 1;
# Reaction rules
react new =
N{v,t} || E{t} || I
->
id || E{t} || I.(V{v,t} | id)
@ [0,1,1,2];
#Initial state
big arch = E{t0}.P{p0} | I.1;
big rcfs = N{v0,t0}.1;
big sys = arch | rcfs;
#System
begin brs
init sys;
rules = [ {new} ];
end