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

atm PEBBLE(Set<String> pebbles,Set<List<String>> rules,String goal, String[]
           startSet) {
    String[] S = startSet.clone();
    int counter=(int)Math.pow(pebbles.size(),startSet.length);

    state player1 {
        Arrays.sort(S);
        if (Arrays.binarySearch(S,goal)>=0) reject;
        if (counter<0) reject;

        exists{
            for(List<String> rule : rules){
                if(Arrays.binarySearch(S,rule.get(0))>=0 && Arrays.binarySearch(
                   S,rule.get(1))>=0 && Arrays.binarySearch(S,rule.get(2))<0){
                    player2{
                        S[Arrays.binarySearch(S,rule.get(0))]=rule.get(2);
                        counter--;
                    }
                }
            }
        }
    }

    state player2 {
        Arrays.sort(S);
        if (Arrays.binarySearch(S,goal)>=0) accept;
        if (counter<0) reject;

        forall{
            for(List<String> rule : rules){
                if(Arrays.binarySearch(S,rule.get(0))>=0 && Arrays.binarySearch(
                   S,rule.get(1))>=0 && Arrays.binarySearch(S,rule.get(2))<0){
                    player1{
                        S[Arrays.binarySearch(S,rule.get(0))]=rule.get(2);
                        counter--;
                    }
                }
            }
        }
    }
}