}
@Override
public List<ValidatorWarning> checkValidity(Game theGame) throws ValidatorException {
try {
StateMachine sm = new ProverStateMachine();
sm.initialize(theGame.getRules());
AimaProver prover = new AimaProver(theGame.getRules());
GdlSentence basesQuery = GdlPool.getRelation(BASE, new GdlTerm[] {X});
Set<GdlSentence> bases = prover.askAll(basesQuery, Collections.<GdlSentence>emptySet());
GdlSentence inputsQuery = GdlPool.getRelation(INPUT, new GdlTerm[] {X, Y});
Set<GdlSentence> inputs = prover.askAll(inputsQuery, Collections.<GdlSentence>emptySet());
if (bases.size() == 0) {
throw new ValidatorException("Could not find base propositions.");
} else if (inputs.size() == 0) {
throw new ValidatorException("Could not find input propositions.");
}
Set<GdlSentence> truesFromBases = new HashSet<GdlSentence>();
for (GdlSentence base : bases) {
truesFromBases.add(GdlPool.getRelation(TRUE, base.getBody()));
}
Set<GdlSentence> legalsFromInputs = new HashSet<GdlSentence>();
for (GdlSentence input : inputs) {
legalsFromInputs.add(GdlPool.getRelation(LEGAL, input.getBody()));
}
if (truesFromBases.isEmpty() && legalsFromInputs.isEmpty()) {
return ImmutableList.of();
}
MachineState initialState = sm.getInitialState();
MachineState state = initialState;
long startTime = System.currentTimeMillis();
while (System.currentTimeMillis() < startTime + millisecondsToTest) {
//Check state against bases, inputs
if (!truesFromBases.isEmpty()) {
if (!truesFromBases.containsAll(state.getContents())) {
Set<GdlSentence> missingBases = new HashSet<GdlSentence>();
missingBases.addAll(state.getContents());
missingBases.removeAll(truesFromBases);
throw new ValidatorException("Found missing bases: " + missingBases);
}
}
if (!legalsFromInputs.isEmpty()) {
List<GdlSentence> legalSentences = new ArrayList<GdlSentence>();
for (Role role : sm.getRoles()) {
List<Move> legalMoves = sm.getLegalMoves(state, role);
for (Move move : legalMoves) {
legalSentences.add(GdlPool.getRelation(LEGAL, new GdlTerm[] {role.getName(), move.getContents()}));
}
}
if (!legalsFromInputs.containsAll(legalSentences)) {
Set<GdlSentence> missingInputs = new HashSet<GdlSentence>();
missingInputs.addAll(legalSentences);
missingInputs.removeAll(legalsFromInputs);
throw new ValidatorException("Found missing inputs: " + missingInputs);
}
}
state = sm.getRandomNextState(state);
if (sm.isTerminal(state)) {
state = initialState;
}
}
} catch (MoveDefinitionException mde) {
throw new ValidatorException("Could not find legal moves while simulating: " + mde);