The complete search is added as package to the jpf-psyco project.

The packet structure is as follows:

gov.nasa.jpf.psyco.search -> collections ->region ->region.util ->util

During the gsoc project, I have implemented different data structures to represent a region. They are all in the region subpackage. On each of this data structure a few operations are needed which are provided by the region.util subpackage. Region and Region.util use jConstraint to represent Expressions for state description. Further the solver abstraction from jConstraint is used to approve expression's satisfiability.

For the Quantifier elimination I created the Interface gov.nasa.jpf.constraints.api.QuantifierEliminator. The NativeZ3Solver has been extended to implement this new Interface. Further jpf-jConstraints-z3 is extended by the NativeZ3TojConstraintConverter to transform z3Expressions back to jConstraint expressions. This is needed for the quantifier elimination.

So far the GSOC project has modified three existing JPF projects.

Data Structures

The algorithm operates mainly on the data structures SymbolicState, which is at basis a Set of SymbolicStates, similar to a Valuation.

SymbolicStates are collected in a SymbolicRegion, which is an extended HashSet. Additonal, there is support for the functions defined on Regions at page with initial thoughts.

Symbolic Search Algorithm Structure

#!java

Required:
transitionSystem : List<Path>
initalState : Valuation

setup_step(initialState):
reachableRegion: SymbolicRegion = new SymbolicRegion
reachableRegion.add(initialState)
newRegion: SymbolicRegion = reachableRegion
k= 0 //Keeps track on k for psyco later.

executeSearch():
    while(newRegion not empty){
        k++;
        possibleNewStates = post(newRegion, transitionSystem);
        newStates = difference(possibleNewStates, reachableRegion);
        reachableRegion = disjunction(newStates, reachableRegion);
    }
    return rechableRegion


//post applies the transitionSystem that is a list of Paths to each state in newRegion.
post(newRegion, transitionSystem):
    oldVariableNames: Set = getVariables(newRegion)
    newPrimeRegion: SymbolicRegion = new SymbolicRegion
    for(path in transitionSystem){
        for(state in newRegion){
            newState: SymbolicState = new SymbolicState
            for(variable in state){
                primeVariable = apply(path, variable)
                newState.add(primeVariable)
            }
            newPrimeRegion.add(newState)
        }
    }
    newPrimeRegion = exists(newPrimeRegion, oldVariableNames)
    newPrimeRegion = rename(newPrimeRegion, oldVariableNames) 
    return newPrimeRegion

//apply add the path result to the value of the variable.
//path consists of a pathCondtion that is the guard and a postcondition
apply(path, variable):
    newVariable: variable = new Variable(variable.getName() +  "'") 
    if(variable.getValue() && path.getPathCondition() ==SAT){
        newValue:Expression = variable.getValue()
        //We don't add the path condition if it is the constant true.
        //State description would be longer without knowledge gain.
        if(path.getPathCondition() != constant("true")){
            newValue = and(newValue, path.getPathCondition())
        }
        newValue = and(newValue, path.getPostCondition(variable))
    }
    newVariable.setValue(newValue)
    return newVariable

//returns states that have a value so that newRegion && not(reachableRegion) is satisfiable.
difference(newRegion, reachableRegion):
    result: SymbolicRegion = new SymbolicRegion
    notRegion: Expression = reachableRegion.toExpression()
    notRegion = new Negation(notRegion)
    //getStateVariables returns all variables in the region, that are part of the state description
    stateVariables = reachableRegion.getStateVariables()
    notRegion = bindParameters(notRegion, stateVariables, Quantifier.FORALL)
    for(state in newRegion){
        testDifferenceExpr = state.toExpression()
        testDifferenceExpr = bindParameters(testDifferenceExpr, stateVariables, Quantifier.EXISTS)
        testDifferenceExpr = and(testDifferenceExpr, notRegion)
        if(isSatisfiable(testDifferenceExpr)){
            result.add(state)
        }
    }
    return result

//binds each variable in stateVariables to the specified quantifierType (all or exist) in the expression
bindParameters(expression, stateVariables, quantifierType)
    toBeBound = []
    for(freeVariable in expression){
        if(freeVariable not in stateVariables){
            toBeBound.add(freeVariable)
        }
    }
    //QuantifierExpression adds to the expression a quantifier of 
    //type quantifierType for each variable in bound.
    quantifierExpression = new QuantifierExpression(quantifier, bound, expression)
    return quantifierExpression

//disjunction is implemented as inclusive disjunction, so it is just the result of regionA or regionB
disjunction(regionA, regionB):
    disjunctedRegion = new SymbolicRegion
    for(state in regionA){
        disjunctedRegion.add(state)
    }
    for(state in regionB){
        disjunctedRegion.add(state)
    }
    return disjunctedRegion

//returns a region with all states if reachableRegion, that contains 
//at least one state variable not in excludedVariables
exists(region, variables):
    existingNewRegion = new SymbolicRegion
    for(state in region){
        newState = new SymbolicState
        for(variable  in state){
            if(variable not in variables){
                existingNewRegion.add(state)
                break
            }
        }
    }
    return existingNewRegion

//rename replaces all occurences of primeNames by oldVariableNames 
//in the region, but calculates the primeNames first
rename(region, oldVariableNames):
    primeNames = []
    for(variable in oldVariableNames){
        newName = variable.getName() + "'"
        primeNames.add(newName)
    }
    region = rename(region, primeNames, oldVariableNames)
    return region

//rename replaces all occurrences of primeNames by oldVariableNames in the region
rename(region, primeNames, oldVariableNames):
    for(state in region){
        for(int i = 0; i < primeNames, i++){
            oldName = oldVariableNames.get(i)
            primeName = primeNames.get(i) 
            //uniqueName generates a String that must be unique.
            //Therefore a continuous counter is added to uVarReplacement.
            //As long as no variable is named uVarReplacement_x, where x is an integer,
            // this name is guaranteed to be unique.
            uniqueReplacement = uniqueName()
            for(variable in region){
                value = variable.getValue()
                //The second parameter is replaced with the third parameter in the expression
                value = renameInExpression(value, oldName, uniqueReplacement)
                value = renameInExpression(value, primeName, oldName)
                variable.setValue(value)
            }
        }
    }
    return region

Symbolic Search Algorithm Structure

#!java

variable = (name, value)
state = []
region = HashMap()

Required:
transitionSystem : List<Path>
initalState : List<variable>

//setup initialize the internal tool structure.
//initial state is a list of variables, each have a name and a start value.
setup_step(initialState):
    reachableRegion = new HashMap()
    reachableRegion.add(initialState)
    newRegion = reachableRegion
    k= 0 //Keeps track on k for psyco later.

//execute search 
executeSearch():
    while(newRegion not empty){
        k++;
        possibleNewStates = post(newRegion, transitionSystem);
        newStates = possibleNewStates && !reachableRegion
        reachableRegion = newStates || reachableRegion
    }
    return rechableRegion

//post applies the transitionSystem that is a list of Paths to each state in newRegion.
post(newRegion, transitionSystem):
    //getVariables(aHashSet) returns the variable used for state description in the HashSet.
    oldVariableNames: Set = getVariables(newRegion)
    //
    newPrimeRegion = new HashSet
    for(path in transitionSystem){
        for(state in newRegion){
            newState = []
            for(variable in state){
                primeVariable = apply(path, variable)
                newState.add(primeVariable)
            }
            newPrimeRegion.add(newState)
        }
    }
    newPrimeRegion = exists(newPrimeRegion, oldVariableNames)
    newPrimeRegion = rename(newPrimeRegion, oldVariableNames) 
    return newPrimeRegion

//apply add the path result to the value of the variable.
//path consists of a pathCondtion that is the guard and a postCondition
apply(path, variable):
    newVariable: variable = variable(variable.getName() +  "'", null) 
    if(isSatisfiable(variable.value && path.getPathCondition())){
        newValue = variable.value
        //We don't add the path condition if it is the constant true.
        //State description would be longer without knowledge gain.
        if(path.getPathCondition() != constant("true")){
            newValue = newValue && path.getPathCondition()
        }
        //The path has one post condition for each variable, that is selected this way.
        newValue = newValue && path.getPostCondition(variable.name)
    }
    newVariable.value = newValue
    return newVariable

//returns a region with all states if reachableRegion, that contains 
//at least one state variable not in excludedVariables
exist(reachableRegion, excludedVariables):
    newRegion = new HashSet
    for(state in reachableRegion){
        if(exist variable: variable element state && not(variable element excludedVariables){
            newRegion.add(state)
        }
    }
    return newRegion


//rename replaces all occurrences of primeNames by oldVariableNames 
//in the region, but calculates the primeNames first
rename(region, oldVariableNames):
    primeNames = []
    for(variable in oldVariableNames){
        newName = variable.getName() + "'"
        primeNames.add(newName)
    }
    region = rename(region, primeNames, oldVariableNames)
    return region

//rename replaces all occurrences of primeNames by oldVariableNames in the region
rename(region, primeNames, oldVariableNames):
    for(state in region){
        for(int i = 0; i < primeNames, i++){
            oldName = oldVariableNames.get(i)
            primeName = primeNames.get(i) 
            //uniqueName generates a String that must be unique.
            //Therefore a continuous counter is added to uVarReplacement.
            //As long as no variable is named uVarReplacement_x, where x is an integer,
            // this name is guaranteed to be unique.
            uniqueReplacement = uniqueName()
            for(variable in region){
                value = variable.getValue()
                //The second parameter is replaced with the third parameter in the expression
                value = renameInExpression(value, oldName, uniqueReplacement)
                value = renameInExpression(value, primeName, oldName)
                variable.setValue(value)
            }
        }
    }
    return region

Comparison Text Book

Due to our representation of the transition system, post differs from the text book. The current implementation does not calculate a conjunction on the reachable region and the transition system. It applies the transition system step-by-step. Currently there is still the exist step in the post method, but I am quite convinced, that it is not necessary anymore due to the implementation of apply. We will have to think about it.

The algorithm uses existentially quantification to merge a state and the transition effect into a new state description containing only prime Variables and rename the prime Variables later to the original state variables. This is not mirrored by the current implementation. That is the reason for the derivation in the implementation of rename. I just keep the old value description of the variable and extend it by the transition effect. The old variable is renamed to a unique name and the prime name is renamed to the old variable name.

That are the main derivations.

Wiki

psyco_gsoc16 / Architectural Overview Algorithm

Data Structures

Symbolic Search Algorithm Structure

Symbolic Search Algorithm Structure

Comparison Text Book