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

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

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

            // check invariant

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

        }

        return false;// TODO
    }
}

@@ -577,24 +577,63 @@
 Stack%3C%3E();%0A%0A
+        // prepare initial state value%0A
         Sing
@@ -1160,24 +1160,342 @@
 pression);%0A%0A
+        Map%3CString, Expr%3E initialStateValue = new HashMap%3C%3E();%0A%0A        BoolExpr invariant;%0A%0A        // prepare initial state value%0A        initialStateValue.put(initialization.getIdentifier().getName(), initialValueConstraint);%0A%0A        // insert initial state%0A        queue.add(new State(null, initialStateValue));%0A%0A
         whil

prepare and insert initial state