partial
open override fun partialCheck(graph: Graph, symbolTable: SymbolTable, variableAssignments: Map<String, Node>, shouldBeModel: Boolean): ModelCheckerTrace(source)
Checks if consequent holds or antecedent does not hold. firstOperand is only checked if secondOperand does not hold.
Return
ModelCheckerTrace that contains the results of this check.
Parameters
graph
The Graph that will be checked.
symbol
SymbolTable that contains all symbols of the parsed root formula and graph.
variable
Map of BoundVariable names and their assigned Nodes.
should
Indicates the expected result. Can be false for subformulas of Operator.Unary.Negation.