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

cyclic atm PEBBLE2 (Set<String> pebbles,Set<List<String>> rules,String goal,
                    String[] startSet) {
    String[] S = startSet.clone();

    state player1 {
        Arrays.sort(S);
        if (Arrays.binarySearch(S,goal)>=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);
                    }
                }
            }
        }
    }

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

        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);
                    }
                }
            }
        }
    }
}