package de.bmoth.modelchecker;

import com.microsoft.z3.Expr;

import java.util.Map;

/**
 * Created by krings on 28.04.17.
 * fixed by hansen on 28.04.17.
 */
public class State {
    State predecessor;
    Map<String, Expr> values;

    public State(State predecessor, Map<String, Expr> values) {
        this.predecessor = predecessor;
        this.values = values;
    }
}

@@ -21,24 +21,91 @@
 elchecker;%0A%0A
+import com.microsoft.z3.BoolExpr;%0Aimport com.microsoft.z3.Context;%0A
 import com.m
@@ -434,11 +434,456 @@
 s;%0A    %7D
+%0A%0A    public BoolExpr getValuesExpression(Context context) %7B%0A        BoolExpr result = null;%0A        for (Map.Entry%3CString, Expr%3E entry : values.entrySet()) %7B%0A            BoolExpr singleExpression = (BoolExpr) entry.getValue();%0A%0A            if (result == null) %7B%0A                result = singleExpression;%0A            %7D else %7B%0A                result = context.mkAnd(result, singleExpression);%0A            %7D%0A        %7D%0A        return result;%0A    %7D
 %0A%7D%0A

enable State to generate a combined BoolExpr of it's stored values