package de.bmoth.modelchecker;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.Sort;
import de.bmoth.backend.FormulaTranslator;
import de.bmoth.parser.ast.nodes.*;

import java.util.*;

/**
 * Created by krings on 28.04.17.
 */
public class ModelChecker {
    public static boolean doModelCheck(MachineNode machine) {
        Context ctx = new Context();
        FormulaTranslator translator = new FormulaTranslator(ctx);

        Set<State> visited = new HashSet<>();
        Stack<State> queue = new Stack<>();

        // prepare initial state value

        // TODO implement FormulaTranslator::visitSingleAssignSubstitution(...)
        // BoolExpr initialValueConstraint = translator.visitSingleAssignSubstitution(initialization,null);

        // TODO take care of other types of SubstitutionNodes
        SingleAssignSubstitution initialization = (SingleAssignSubstitution) machine.getInitialisation();
        ExprNode initialValue = initialization.getValue();

        Expr initialValueAsZ3Expression = translator.translateExpression(initialValue);
        Sort z3TypeOfInitialValue = translator.bTypeToZ3Sort(initialValue.getType());

        Expr theIdentifier = ctx.mkConst(initialization.getIdentifier().getName(), z3TypeOfInitialValue);

        BoolExpr initialValueConstraint = ctx.mkEq(theIdentifier, initialValueAsZ3Expression);

        Map<String, Expr> initialStateValue = new HashMap<>();

        BoolExpr invariant;

        // prepare initial state value
        initialStateValue.put(initialization.getIdentifier().getName(), initialValueConstraint);

        // insert initial state
        queue.add(new State(null, initialStateValue));

        while (!queue.isEmpty()) {
            State current = queue.pop();

            // check invariant

            // compute successors
            // add to queue if not in visited

        }

        return false;// TODO
    }
}

@@ -53,109 +53,9 @@
 .z3.
-BoolExpr;%0Aimport com.microsoft.z3.Context;%0Aimport com.microsoft.z3.Expr;%0Aimport com.microsoft.z3.Sort
+*
 ;%0Aim
@@ -318,24 +318,64 @@
  Context();%0A
+        Solver solver = ctx.mkSolver();%0A
         Form
@@ -1670,24 +1670,966 @@
 teValue));%0A%0A
+        // prepare invariant%0A        %7B%0A            PredicateNode invariantNode = machine.getInvariant();%0A%0A            // TODO this is ugly, we need a top level method here!%0A            if (invariantNode instanceof PredicateOperatorNode) %7B%0A                invariant = (BoolExpr) translator.visitPredicateOperatorNode((PredicateOperatorNode) invariantNode, null);%0A            %7D else if (invariantNode instanceof PredicateOperatorWithExprArgsNode) %7B%0A                invariant = (BoolExpr) translator.visitPredicateOperatorWithExprArgs((PredicateOperatorWithExprArgsNode) invariantNode, null);%0A            %7D else %7B%0A                throw new AssertionError(%22Invariant generating not implemented for: %22 + invariantNode.getClass());%0A            %7D%0A%0A            solver.add(invariant);%0A%0A            if (solver.check() != Status.SATISFIABLE) %7B%0A                throw new AssertionError(%22Invariant not satisfiable:%22 + invariant);%0A            %7D%0A        %7D%0A%0A
         whil

prepare and check invariant, introducing solver