ISPL Examples

You'll probably prefer to write pythonic ISPL, but this page inlines some examples of raw ISPL for study/reference. The first example focuses on minimalism. The second example is the classic muddy children puzzle, one of many examples that ship with the mcmas engine source code1.

Minimal Example

The goal for this example is to exercise the mcmas engine as a solver for simple logic, basically ignoring the ISPL language capabilities for other things like agents and time-evolution. Nevertheless we need an agent and rules for time-evolution anyway just to have legal ISPL, so this sets up enough scaffolding for a "trivial" Agent that does nothing, then validates a few simple logical expressions.

Summary 
-- Minimal ISPL specification
-- See the docs https://mattvonrocketstein.github.io/py-mcmas/ispl#minimal

Agent Environment
    Vars:
      p: boolean;
      q: boolean;
    end Vars
    Actions = {tick};
    Protocol:
      Other : {tick};
    end Protocol
    Evolution:
    end Evolution
end Agent

Agent DefaultAgent
    Vars:
      ticking: boolean;
    end Vars
    Actions = {tick};
    Protocol:
      Other : {tick};
    end Protocol
    Evolution:
        ticking=true if Action=tick;
    end Evolution
end Agent

Evaluation
  p if Environment.p=true;
  q if Environment.q=true;
end Evaluation

InitStates
  Environment.p=true and Environment.q=false;
end InitStates

Formulae
  p; !q; 
  p -> !q;
end Formulae

The pythonic equivalent is more succinct and flexible, but the verbose version here illustrates more of the primitives. See the ISPL Reference for: Environment, Agent, Evaluation, Init-States, Formulae

Muddy Children

Introducing agents and knowledge with Muddy-children is traditional.

ISPL References: Environment, Agent, Evaluation, Init-States, Formulae

Logic Operator Reference: AG(..), K(..)

Summary 
-- The protocol for the 3 muddy children
Agent Environment
  Obsvars:
    sayexist: boolean;
    mem: -1..2;
  end Obsvars
  Vars:
    initial: boolean;
    child1: 0..1;
    child2: 0..1;
    child3: 0..1;
  end Vars
  Actions = { exists, ask };
  Protocol:
    initial=true and (child1=1 or child2=1 or child3=1): {exists};
    Other: {ask};
  end Protocol
  Evolution:
    initial=false and sayexist=true and mem = mem + 1 
      if initial=true and Action=exists;
    initial=false and mem = mem + 1 
      if initial=true and Action=ask;
    mem = mem + 1 if initial=false and mem < 2;
  end Evolution
end Agent

Agent Child1
  Lobsvars = { child2, child3 };
  Vars:
    othersayknow: boolean;
  end Vars
  Actions = { donotknow, know };
  Protocol:
    Environment.mem<Environment.child2+Environment.child3: {donotknow};
    Environment.mem>=Environment.child2+Environment.child3: {know};
  end Protocol
  Evolution:
    othersayknow=true 
      if Environment.Action=ask and 
        Environment.mem<Environment.child2+Environment.child3 and 
        othersayknow=false and 
        (Child2.Action=know or Child3.Action=know);
  end Evolution
end Agent

Agent Child2
  Lobsvars = { child1, child3 };
  Vars:
    othersayknow: boolean;
  end Vars
  Actions = { donotknow, know };
  Protocol:
    Environment.mem<Environment.child1+Environment.child3: {donotknow};
    Environment.mem>=Environment.child1+Environment.child3: {know};
  end Protocol
  Evolution:
    othersayknow=true 
      if Environment.Action=ask 
      and Environment.mem<Environment.child1+Environment.child3 
      and othersayknow=false 
      and (Child1.Action=know or Child3.Action=know);
  end Evolution
end Agent

Agent Child3
  Lobsvars = { child1, child2 };
  Vars:
    othersayknow: boolean;
  end Vars
  Actions = { donotknow, know };
  Protocol:
    Environment.mem<Environment.child1+Environment.child2: {donotknow};
    Environment.mem>=Environment.child1+Environment.child2: {know};
  end Protocol
  Evolution:
    othersayknow=true 
    if Environment.Action=ask 
      and Environment.mem<Environment.child1+Environment.child2 
      and othersayknow=false 
      and (Child1.Action=know or Child2.Action=know);
  end Evolution
end Agent

Evaluation
  muddy1 if Environment.child1=1;
  muddy2 if Environment.child2=1;
  muddy3 if Environment.child3=1;
  saysknows1 
    if Environment.child2+Environment.child3<=Environment.mem;
  saysknows2 
    if Environment.child1+Environment.child3<=Environment.mem;
  saysknows3 
    if Environment.child1+Environment.child2<=Environment.mem;
end Evaluation

InitStates
  Child1.othersayknow=false and Child2.othersayknow=false 
  and Child3.othersayknow=false and Environment.sayexist=false 
  and Environment.initial=true and Environment.mem=-1;
end InitStates

Formulae
  AG((saysknows1 -> 
    (K(Child1, muddy1) or K(Child1, !muddy1))) 
    and ((K(Child1, muddy1) or K(Child1, !muddy1)) -> saysknows1));
  AG((saysknows2 -> 
    (K(Child2, muddy2) or K(Child2, !muddy2))) 
    and ((K(Child2, muddy2) or K(Child2, !muddy2)) -> saysknows2));
  AG((saysknows3 -> 
    (K(Child3, muddy3) or K(Child3, !muddy3))) 
    and ((K(Child3, muddy3) or K(Child3, !muddy3)) -> saysknows3));
end Formulae

References

  1. ISPL examples that ship with the engine source ↩

  2. Reasoning About Knowledge, Fagin et al ↩