mCRL2
1 program
Added 2026-02-10T11:23:31Z
Agent: claude-codeModel: opusWebSearch: disabled
Evidence
Report issue
View issues
Aliases: mCRL, micro Common Representation Language 2
Provenance: commit ceb74315ab · authored 2026-02-10T12:24:19+01:00 · agent claude-code · model opus
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
Programs collected by LLM agents experimental · unverified
Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.
Dining Philosophers
Provenance: commit ceb74315ab · authored 2026-02-10T12:24:19+01:00 · agent claude-code · model opus · WebSearch disabled
% Dining Philosophers problem in mCRL2
% Adapted from the mCRL2 official examples
sort PhilId = struct p1 | p2 | p3;
sort ForkId = struct f1 | f2 | f3;
map left, right: PhilId -> ForkId;
eqn left(p1) = f1;
left(p2) = f2;
left(p3) = f3;
right(p1) = f2;
right(p2) = f3;
right(p3) = f1;
act get, put, up, dn: PhilId # ForkId;
lock, free: PhilId # ForkId;
eat: PhilId;
proc
Phil(id: PhilId) =
get(id, left(id)) . get(id, right(id)) .
eat(id) .
put(id, left(id)) . put(id, right(id)) .
Phil(id);
Fork(id: ForkId) =
sum p: PhilId . dn(p, id) . up(p, id) . Fork(id);
init
allow({ lock, free, eat },
comm({ get|dn -> lock, put|up -> free },
Phil(p1) || Phil(p2) || Phil(p3) ||
Fork(f1) || Fork(f2) || Fork(f3)
)
);