Ltl2SmvPrefixes Struct Reference

A function to run ltl2smv routine. More...

#include <ltl2smv.h>

Data Fields
char *	ltl_module_base_name
char *	pre_prefix
char *	prefix_name

---

Detailed Description

A function to run ltl2smv routine.

Author:

Andrei Tchaltsev, Marco Roveri Here we perform a convertion from LTL formula to SMV module. The invoker provides the LTL fromula in the form of node_ptr expression. The function 'ltl2smv' will convert this formula to a SMV module, which is also node_ptr MODULE.

This file provides routines for reducing LTL model checking to CTL model checking. This work is based on the work presented in \[1\]

• O. Grumberg E. Clarke and K. Hamaguchi. <cite>Another Look at LTL Model Checking</cite>. Formal Methods in System Design, 10(1):57--71, February 1997.

---

Field Documentation

char* Ltl2SmvPrefixes::ltl_module_base_name

char* Ltl2SmvPrefixes::pre_prefix

char* Ltl2SmvPrefixes::prefix_name

---

The documentation for this struct was generated from the following file:

• NuSMV/code/nusmv/core/ltl/ltl2smv/ltl2smv.h