% crochet

local type person;
local singleton karis is person;
local singleton lielle is person;

local enum state = greet, part, halt;

relation Person* state: State;
relation output: Output*;


action karis say-hello-karis
when karis state: greet do
  fact output: "[karis] says: Hello!";
end

action lielle say-hello-lielle
when lielle state: greet do
  fact output: "[lielle] greets in kind.";
end

action (P is person) part
when P state: part do
  fact output: "[P] leaves.";
end

when P simulate-turn, P state: S, if S < state upper-bound do
  fact P state: (S successor);
end

test "Simulations respect turn ordering and action restrictions" do
  fact karis state: greet;
  fact lielle state: greet;
  simulate for [karis, lielle] until action quiescence;
  assert (search output: Output) =:= [
    [Output -> "[karis] says: Hello!"],
    [Output -> "[lielle] greets in kind."],
    [Output -> "[karis] leaves."],
    [Output -> "[lielle] leaves."]
  ];
end