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

acyclic atm Horn3(int goal, Map<Integer, Set<Set<Integer>>> rules) {
int head=goal;
Set<Integer> body;
int counter=rules.keySet().size();

state head{
    // catch cycles
    if (counter<0){
        reject;
    } else {
        counter--;
    }
    exists{
            for(Set<Integer> rule: rules.get(head)){
                body{
                    head=0;
                    body=rule;
                }
            }
    }
}

state body {
    forall{
        for(Integer literal: body){
            head{
                head=literal;
                body=null;
            }
        }
    }
}


}