apollo-backend/eu.yeger.apollo.shared.model.fol/ModelCheckerTrace

ModelCheckerTrace

data class ModelCheckerTrace(val formula: String, val description: TranslationDTO, val isModel: Boolean, val shouldBeModel: Boolean, val children: List<ModelCheckerTrace>? = null)(source)

Trace of the ModelChecking algorithm. Contains information about a single check and its child checks.

Author

Jan Müller

Constructors

ModelCheckerTrace

constructor(formula: String, description: TranslationDTO, isModel: Boolean, shouldBeModel: Boolean, children: List<ModelCheckerTrace>? = null)

Creates a ModelCheckerTrace with the given parameters.

Properties

val children: List<ModelCheckerTrace>? = null

List of child-traces.

val description: TranslationDTO

TranslationDTO with a description key for this check.

val formula: String

The String representation of the checked Formula.

val isModel: Boolean

Indicates that the Graph is a model of the checked formula.

val shouldBeModel: Boolean

Indicates that the Graph is supposed to be model of checked formula.