Jonathan Certes

Home / Resources / Walk the AST and access names of specifications with pyNUSMV

Introduction

NuSMV is an open-source model checker which implements symbolic model-checking, using a fixed point algorithm with Binary Decision Diagrams (BDD), where a set of states is represented by a BDD instead of an exhaustive list of individual states. Models are described in SMV language and NuSMV supports the analysis of specifications expressed as invariants or in temporal logics, including LTL and PSL.

pyNuSMV is a Python binding for NuSMV. It is intended to provide a Python interface to NuSMV, allowing to use NuSMV as a library.

Properties in SMV language

Let's imagine that we have several properties that we formally verify with NuSMV. We give names to theses properties so that we can have a translation in natural language. SMV language allows to do so with the NAME attribute.

LTLSPEC
  NAME = "We eventually reach 15." :=
    F ("counter" = 0ub4_1111);

PSLSPEC
  NAME = "If the counter is set to 0, then it is set to 1 at next step." :=
    always( ("counter" = 0ub4_0000) -> next("counter" = 0ub4_0001) );

To write the documentation of our system, we would like to extract all the names from all our properties. This can be achieved by walking the Abstract Syntax Tree (AST) of the SMV model and extract the names from the appropriate nodes.

Python script with pyNUSMV

We can write a function in Python to find all nodes of a particular type (for example: LTLSPEC). This is a recursive function to append all nodes of a given type to a list:

def recursivelyGetAllNodes(
  theTopNode,   #!< the node to get in the hierarchy from
  theNodeType,  #!< the type of nodes to add to the list
  theList       #!< the list to append
):
  if ( theTopNode.type == theNodeType ):
    list.append(theList, theTopNode)
  else:
    if theTopNode.type not in {
      pynusmv.nusmv.parser.parser.NUMBER_SIGNED_WORD,
      pynusmv.nusmv.parser.parser.NUMBER_UNSIGNED_WORD,
      pynusmv.nusmv.parser.parser.NUMBER_FRAC,
      pynusmv.nusmv.parser.parser.NUMBER_EXP,
      pynusmv.nusmv.parser.parser.NUMBER_REAL,
      pynusmv.nusmv.parser.parser.NUMBER,
      pynusmv.nusmv.parser.parser.ATOM,
      pynusmv.nusmv.parser.parser.FAILURE
    }:
      if ( pynusmv.nusmv.node.node.car(theTopNode) is not None ):
        recursivelyGetAllNodes( pynusmv.nusmv.node.node.car(theTopNode),
                                theNodeType,
                                theList
                              )
      if ( pynusmv.nusmv.node.node.cdr(theTopNode) is not None ):
        recursivelyGetAllNodes( pynusmv.nusmv.node.node.cdr(theTopNode),
                                theNodeType,
                                theList
                              )

Then, we can write a function to parse a file written in SMV language, using the parser from NuSMV, and print the names of all properties in it.

def specnames_parseSmvFile(
  theFilePath #!< path to the input file containing PSL expressions
):
  pynusmv.init.reset_nusmv()
  # causes a segmentation fault if the input file is not correctly written
  # (catching the error cannot avoid NuSMV API to stop):
  pynusmv.nusmv.parser.parser.Parser_ReadSMVFromFile(str(theFilePath))

  # accesses all specification properties in the file:
  theTree = pynusmv.nusmv.parser.parser.cvar.parsed_tree
  theList = list()
  recursivelyGetAllNodes(theTree, pynusmv.nusmv.parser.parser.PSLSPEC,  theList)
  recursivelyGetAllNodes(theTree, pynusmv.nusmv.parser.parser.LTLSPEC,  theList)
  recursivelyGetAllNodes(theTree, pynusmv.nusmv.parser.parser.INVARSPEC,theList)
  theList.reverse()

  for theSpecNode in theList:
    # saves the name of the property (left node):
    theNameNode   = pynusmv.nusmv.node.node.cdr(theSpecNode)
    theNameString = pynusmv.nusmv.node.node.sprint_node(theNameNode)
    # prints it:
    if ( str.strip(theNameString) != "" ):
      print(theNameString)
      print("")

In the end, we can initialize NuSMV and call our function for all files provided as arguments:

pynusmv.init.init_nusmv()
for theArg in sys.argv[1:len(sys.argv)]:
  specnames_parseSmvFile(theArg)

Makefile

Now, we must call our program and ask it to parse the files containing our specifications. Let's imagine that our program is written in a file called specnames.py and that our specifications are located in a file called counter.smv.

Here is a Makefile that provides the recipe (make sure to indent with tabulations):

all: counter.smv
    ./specnames.py $^

Associated resources

Here is an archive which contains the discussed example and its Makefile.

---