Graded-CTL NuSMV

Implementation Details

New Package Graded: We have introduced a new package called Graded where we have implemented our algorithms and utility functions that we use in the implementation of the model checking algorithm. The package Graded is divided in the following two sub-packages: utils that collects the utility functions that are used in the implementation of the graded-CTL model-checking algorithms and Mc in which are implemented the functions for the model checking.
- ModelChecking.c implements the interface between the NuSMV system and the graded package. It contains only the function GradedMc_checkGradedCtlSpec that performs the calls to verify the graded-ctl formula, to generates the counterexamples and to print them.
- Eval.c in this file there is the code to compile graded-CTL formulas into BDD and the code to call model checking graded algorithms. It contains the following functions:
  1. evalGradedCtlSpec compile a graded-CTL formula and calls the model checking functions.
  2. evalRecur performs the recursive step of the eval_ctl_spec_recur function.
  3. operation1NG performs unary boolean operations.
  4. operation2NG performs binary boolean operations.
  5. operation1GM performs unary graded operations.
  6. operation2GM performs binary graded operations.
- Explain.c in this file there are the functions that needs to compute counterexamples and witness for graded-CTL formulas.
  1. GradedMc_explainGraded given in input a graded-CTL formula, returns the tree containing the witness for it.
  2. GradedMc_explainRecurGraded performs the recursive step of the GradedMc_explainGraded function.
  3. GradedMc_exExplainGraded given in input one set of states g, computes the witness for E>k X g.
  4. GradedMc_euExplainGraded given in input two sets of states f and g, computes the witness for E>k [f U g].
  5. GradedMc_egExplainGraded given in input one set of states g, computes the witness for E>k G g.
  6. exstendPaths is used for formulas of the form E>k X v and E>k [f U v], where v is a graded-CTL formula. The function extend the traces to show a witness for v.
- GradedCtl.c is the main file of the package and contains the implementations of the symbolic algorithms for the graded-CTL model checking.
  1. GradedMc_and: returns a BDD representing the set of states that verify a formula ψ1 ∧ ψ2.
  2. GradedMc_or: returns a BDD representing the set of states that verify a formula ψ1 ∨ ψ2.
  3. GradedMc_not: returns a BDD representing the set of states that verify a formula ¬ ψ1.
  4. GradedMc_xor: returns a BDD representing the set of states that verify a formula ψ1 ⊕ ψ2.
  5. GradedMc_xnor: returns a BDD representing the set of states that verify a formula ψ1 XNOR ψ2. Recall that ψ1 XNOR ψ2 ⇔ ¬(ψ1 ⊕ ψ2).
  6. GradedMc_implies: returns a BDD representing the set of states that verify a formula ψ1 ⇒ ψ2.
  7. GradedMc_iff: returns a BDD representing the set of states that verify a formula ψ1 ⇔ ψ2.
  8. GradedMc_ex: returns a BDD representing the set of states that verify a formula E>k X ψ1.
  9. GradedMc_ax: returns a BDD representing the set of states that verify a formula A≤k X ψ1.
  10. GradedMc_eu: returns a BDD representing the set of states that verify a formula E>k ψ1 U ψ2.
  11. GradedMc_au: returns a BDD representing the set of states that verify a formula A≤k ψ1 U ψ2.
  12. GradedMc_eg: returns a BDD representing the set of states that verify a formula E>k G ψ1
  13. GradedMc_ag: returns a BDD representing the set of states that verify a formula A≤k G ψ1.
  14. GradedMc_ef: returns a BDD representing the set of states that verify a formula E>k F ψ1
  15. GradedMc_af: returns a BDD representing the set of states that verify a formula A≤k F ψ1.
- GradedUtils.c this file is part of graded-utils subpackage and collects the following utility functions that are used in the implementation of the graded-CTL model-checking algorithms.
  1. GradedUtils_nodePlus: compute the sum of two ADD leaves.
  2. GradedUtils_nodeTimes: compute the product of two ADD leaves.
  3. GradedUtils_addApply: given two ADDs f and g and the binary operator *, returns f*g. This function is a bounded leaf-value re-implementation of the CUDD addApply.
  4. GradedUtils_addApplyRecur performs the recursive step of the GradedUtils_addApply function.
  5. GradedUtils_bddIsSubset: given two BDDs A and B, this function returns true if A is a subset of B, false otherwise.
  6. GradedUtils_bddMinus: given two BDDs A and B, this function returns the BDD A\B.
  7. GradedUtils_getCleanTransition: given a set of transition T, this fucntion abstract input variables away from T.
  8. GradedUtils_euGetIntermediateSets: computes the sets E>0 ψ1 U ψ2,..., E>k ψ1 U ψ2.
  9. GradedUtils_egGetIntermediateSets: computes the sets E>0 G ψ1,..., E>k G ψ1.
  10. GradedUtils_node_ptrToTreeNode_ptr: given a trace transform it in a tree.
  11. GradedUtils_printPaths: given a tree of paths, this function prints it.
  12. GradedUtils_printPathsRecur performs the recursive step of the GradedUtils_printPaths function.
  13. GradedUtils_findCycle: given a tree of paths, this function finds the cycles in the paths.
  14. GradedUtils_findCycleRecur performs the recursive step of the GradedUtils_findCycle function.
  15. GradedUtils_countTraces: given a tree of paths, this function counts the number of paths.
  16. GradedUtils_fsmCountSuccessors: given a subset of states X of S returns the number of successor that each state of S have in X.
  17. GradedUtils_fixPoint: fixed point algorithm.
  18. GradedUtils_applyReachableAndMask: given a set of states S applies the mask and removes not reachable states.
  19. GradedUtils_applyReachableAndMaskToTransition: given a set of transition S applies the mask and removes transition between not reachable states.
  20. GradedUtils_getKBackwardImage: given a set of states f and an integer k, this function returns the set of states g with at least k successors in f.
  21. GradedUtils_bddPickOneState: given a set of states f, this function picks a state from the set f.
  22. GradedUtils_bddPickOneMintermNR : this function is used from GradedUtils_bddPickOneState.
  23. GradedUtils_AddAndAbstract: this function is the implementation of the relational product for ADDs.
  24. GradedUtils_AddAndAbstractRecur performs the recursive step of the GradedUtils_AddAndAbstract function.
- TreeUtils.c in this file there is the code to manipulate the tree node structure used during the counterexamples generation and print operations.
  1. TreeUtils_treeNodeCreate given a state and an input as BDDs, this function create a TreeNode that incapsulate(controllare) them.
  2. TreeUtils_concat given two treeNode root and child, this function append child to the children list of root.
  3. TreeUtils_getState returns the state field of a treeNode.
  4. TreeUtils_getInput returns the input field of a treeNode.
  5. TreeUtils_getListaFigli returns the children list of a treeNode.
  6. TreeUtils_getNext returns the next child in the children list given in input.
  7. TreeUtils_getNodo returns the current treeNode child in the children list given in input.

Cudd package: We have modified the CUDD package with a re-implementation and an extension of the cache to allow the storage of grading values. In particular our bounded leaf-value implementation of the operation on ADDs needs to store entry with more than three operands and this was impossible before our modification of the CUDD package.
- cuddInt.h
  1. Added the constants DD_ADD_NODE_TIMES_TAG, DD_ADD_NODE_PLUS_TAG e DD_ADD_NODE_ANDABSTRACT_TAG.
  2. Defined the new structure GradedCache.
  3. Declared the functions Graded_CHash e Graded_CHash3.
  4. Defined the functions GradedUtils_cacheInit, GradedUtils_cacheFlush, GradedUtils_cacheIsert4, GradedUtils_cacheInsert3, GradedUtils_cacheLookup4 e GradedUtils_cacheLookup3.
- cuddTable.c
  1. Added the call to GradedUtils_cacheFreeDeadNodes in the cuddgarbageCollect function.
- cuddInit.c
  1. Added the call to GradedUtils_cacheInit in the Cudd_Init function.
- GradedUtilsCache.c implements the GradedCTL cache.
  1. Function GradedUtils_cacheInit initializes the cache.
  2. Function GradedUtils_cacheFlush flushes the cache.
  3. Function GradedUtils_cacheFreeDeadNodes free the cache from dead nodes.
  4. Function GradedUtils_cacheInsert4 inserts an entry with four operands in the cache.
  5. Function GradedUtils_cacheInsert3 inserts an entry with three operands in the cache.
  6. Function cacheLookup4 return the value of an entry with four operands from the cache.
  7. Function cacheLookup3 return the value of an entry with three operands from the cache.