partialCheck

open override fun partialCheck(graph: Graph, symbolTable: SymbolTable, variableAssignments: Map<String, Node>, shouldBeModel: Boolean): ModelCheckerTrace(source)

Checks if both conjuncts hold. secondOperand is only checked if firstOperand holds.

Return

ModelCheckerTrace that contains the results of this check.

Parameters

graph

The Graph that will be checked.

symbolTable

SymbolTable that contains all symbols of the parsed root formula and graph.

variableAssignments

Map of BoundVariable names and their assigned Nodes.

shouldBeModel

Indicates the expected result. Can be false for subformulas of Operator.Unary.Negation.