Coverage Summary for Class: FormulaVisitor (itmo.verifier.visitor)
| Class |
Class, %
|
Method, %
|
Branch, %
|
Line, %
|
Instruction, %
|
| FormulaVisitor |
100%
(1/1)
|
100%
(4/4)
|
100%
(4/4)
|
100%
(5/5)
|
100%
(62/62)
|
package itmo.verifier.visitor
import itmo.verifier.formula.CTLFormula
import itmo.verifier.model.Model
import itmo.verifier.model.State
class FormulaVisitor(val formula: CTLFormula, val kripke: Model) {
val eval: MutableMap<State, MutableMap<CTLFormula, Boolean>> = mutableMapOf()
fun makeEval(state: State, formula: CTLFormula, status: Boolean) {
eval.getOrPut(state) { mutableMapOf() }[formula] = status
}
fun getEval(state: State, formula: CTLFormula): Boolean {
return eval[state]?.get(formula) ?: false
}
fun isVisited(formula: CTLFormula): Boolean {
return eval.values.any { formula in it }
}
}