mod YA-BLOCKS-WORLD is
  protecting MACHINE-INT .
  sorts Block Fact FactSet .
  subsort Fact < FactSet .

  ops blue green red yellow black grey : -> Block [ctor] .   
  op onBlock : Block Block -> Fact [ctor] .
  op onTable : Block -> Fact [ctor] .
  op clear : Block -> Fact [ctor] .
  op factSet : FactSet FactSet -> FactSet [ctor assoc comm] .
  op size : Block -> MachineInt .

  eq size(blue) = 1 .   eq size(green) = 2 .
  eq size(red) =  3 .   eq size(yellow) = 4 .
  eq size(black) = 5 .  eq size(grey) = 6 .

  vars X Y Z : Block .

  *** move a block X from a block Z to the table
  rl [unstack] : factSet(onBlock(X, Z), clear(X)) 
               => factSet(onTable(X), clear(X), clear(Z)) .

  *** move a block X from the table to a block Z
  rl [stack] : factSet(onTable(X), clear(X), clear(Z)) 
             => factSet(onBlock(X, Z), clear(X)) .
 
  *** move a block X from a block Z to another block Y
  rl [move] : factSet(onBlock(X, Z), clear(X), clear(Y)) 
            => factSet(onBlock(X, Y), clear(X), clear(Z)) .   
endm