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 }
     }
 }