package at.ac.tuwien.dbai.alternation.examples;
import java.util.List;
import java.util.Set;
import java.util.Map;

atm OneDimensionalCellularAutomata (char[] cells, int cell, char finalstate, int
                                    T,Byte r, Map<List<Character>,Character>
                                    rphi) {
    List<Character> parents;
    int t=T;
    int position=cell;
    char caState=finalstate;

    //look for rules deriving the state
    state ExistsState {
        if (t==0) {
            if (position>=0 && position<cells.length) {
                if (caState==cells[position]){
                    accept;
                } else {
                    reject;
                }
            } else {
                if (caState=='b'){
                    accept;
                } else {
                    reject;
                }
            }
        }
        exists{
            for (Map.Entry<List<Character>,Character> hilf : rphi.entrySet()){
                if(hilf.getValue().equals(caState)) {
                    ForallState{
                        parents=hilf.getKey();
                    }
                }
            }
        }
    }

    //check preconditions for the selected rule
    state ForallState {
        t--;
        forall {
            for (int i=0 ; i<=2*r; i++){
                ExistsState{
                    position=position-r+i;
                    caState=parents.get(i);
                }
            }
        }
    }
}