% This file contains a generator of state machines for cellular
% automata according to pages 277 and following of Stephen Wolfram's
% book `A new kind of science', Wolfram media, inc. 2002. The automaton
% generated by P(i,s) represents all the sequences of black and white
% squares that exist when applying the cellular automaton represented
% by `rule' i times to any arbitrary such sequence. The state s is
% the initial point.
%
% From a mCRL2 perspective, the description below is interesting
% because it heavily uses functions and sets. As it stands (September
% 2005) the toolset can only generate the automata for i=0. For
% higher i the existential quantifiers need to be resolved, which
% currently is outside the capacities of the mCRL2 tools. This
% specification can therefore best be seen as a challenge for future
% releases of the toolset.

map rule:Bool#Bool#Bool -> Bool;

eqn rule(true,true,true)=true;
    rule(true,true,false)=true;
    rule(true,false,true)=true;
    rule(true,false,false)=true;
    rule(false,true,true)=true;
    rule(false,true,false)=true;
    rule(false,false,true)=true;
    rule(false,false,false)=true;

sort State = Nat -> Bool;
sort Transition = struct trans(src:State,label:Bool,tar:State);
sort Transitions = Nat -> Set(Transition);

map s0:State;
eqn s0=lambda i:Nat.false;

map T:Transitions;
var i:Nat;
eqn T(i)=if(i==0,
           { trans(s0,false,s0),trans(s0,true,s0) },
           { t:Transition |
               exists g,g1:State.
                 (src(t)(2*i+2)==tar(t)(2*i+1) &&
                  rule(src(t)(2*i+1),src(t)(2*i+2),tar(t)(2*i+2))==label(t) &&
                  trans(
                    lambda j:Nat.if(j>=2*i+1,false,src(t)(j)),
                    src(t)(2*i+1),
                    lambda j:Nat.if(j>=2*i+1,false,tar(t)(j))) in T(Int2Nat(i-1)) &&
                  trans(
                    lambda j:Nat.if(j>=2*i+1,false,tar(t)(j)),
                    src(t)(2*i+2),
                    g) in T(Int2Nat(i-1)) &&
                  trans(
                    g,
                    tar(t)(2*i+2),
                    g1) in T(Int2Nat(i-1))) });

act WHITE,BLACK;

proc P(i:Nat,s:State)=
         sum s1:State. (trans(s,true,s1) in T(i)) ->
                       WHITE.P(i,s1)+
         sum s1:State. (trans(s,false,s1) in T(i)) ->
                       BLACK.P(i,s1);

init P(1,s0);
