Implication

class Implication(val firstOperand: Formula, val secondOperand: Formula) : Operator.Binary(source)

Represents an implication operator.

Jan Müller

firstOperand

The antecedent.

secondOperand

The consequent.

Constructors

constructor(firstOperand: Formula, secondOperand: Formula)

Creates an Implication operator with the given antecedents and consequent.

The first/left operand of this binary operator.

The name of the entity.

The second/right operand of this binary operator.

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

Checks if consequent holds or antecedent does not hold.

open override fun getRawString(variableAssignments: Map<String, Node>): String

Returns raw String representation of this binary operator.

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

Checks if consequent holds or antecedent does not hold. firstOperand is only checked if secondOperand does not hold.

override fun toString(): String

Returns a String representation with no variable assignments and no brackets or dot at root level.

fun toString(variableAssignments: Map<String, Node>, wrap: Boolean): String

Returns a String representation with no variable assignments and optional brackets or dot at root level.