Ltl_StructCheckLtlSpec Struct Reference

Routines to handle with LTL model checking. More...

#include <ltl.h>

Related Functions
(Note that these are not member functions.)
void	Ltl_StructCheckLtlSpec_build (Ltl_StructCheckLtlSpec_ptr self)
	Initialize the structure by computing the tableau for the LTL property.
Trace_ptr	Ltl_StructCheckLtlSpec_build_counter_example (Ltl_StructCheckLtlSpec_ptr self, NodeList_ptr symbols)
	Perform the computation of a witness for a property.
void	Ltl_StructCheckLtlSpec_check (Ltl_StructCheckLtlSpec_ptr self)
	Perform the check to see wether the property holds or not.
Ltl_StructCheckLtlSpec_ptr	Ltl_StructCheckLtlSpec_create (NuSMVEnv_ptr env, Prop_ptr prop)
void	Ltl_StructCheckLtlSpec_destroy (Ltl_StructCheckLtlSpec_ptr self)
void	Ltl_StructCheckLtlSpec_explain (Ltl_StructCheckLtlSpec_ptr self, NodeList_ptr symbols)
	Perform the computation of a witness for a property.
bdd_ptr	Ltl_StructCheckLtlSpec_get_clean_s0 (Ltl_StructCheckLtlSpec_ptr self)
	Get the s0 field purified by tableu variables.
bdd_ptr	Ltl_StructCheckLtlSpec_get_s0 (Ltl_StructCheckLtlSpec_ptr self)
	Get the s0 field of an Ltl_StructCheckLtlSpec structure.
void	Ltl_StructCheckLtlSpec_print_result (Ltl_StructCheckLtlSpec_ptr self)
	Prints the result of the Ltl_StructCheckLtlSpec_check fun.
void	Ltl_StructCheckLtlSpec_set_do_rewriting (Ltl_StructCheckLtlSpec_ptr self, boolean do_rewriting)
	Set the do_rewriting field of an Ltl_StructCheckLtlSpec structure.
void	Ltl_StructCheckLtlSpec_set_ltl2smv (Ltl_StructCheckLtlSpec_ptr self, Ltl_StructCheckLtlSpec_ltl2smv ltl2smv)
	Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure.
void	Ltl_StructCheckLtlSpec_set_negate_formula (Ltl_StructCheckLtlSpec_ptr self, boolean negate_formula)
	Set the negate_formula field of an Ltl_StructCheckLtlSpec structure.
void	Ltl_StructCheckLtlSpec_set_oreg2smv (Ltl_StructCheckLtlSpec_ptr self, Ltl_StructCheckLtlSpec_oreg2smv oreg2smv)
	Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure.

---

Detailed Description

Routines to handle with LTL model checking.

Author:

Marco Roveri Here we perform the reduction of LTL model checking to CTL model checking. The technique adopted has been taken from \[1\].

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

Todo:

Missing synopsis

Todo:

Missing description

---

Friends And Related Function Documentation

void Ltl_StructCheckLtlSpec_build

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Initialize the structure by computing the tableau for the LTL property.

Initialize the structure by computing the tableau for the LTL property and computing the cross-product with the FSM of the model.

Trace_ptr Ltl_StructCheckLtlSpec_build_counter_example	(	Ltl_StructCheckLtlSpec_ptr	self,
		NodeList_ptr	symbols
	)			[related]

Perform the computation of a witness for a property.

Perform the computation of a witness for a property. Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build, and that Ltl_StructCheckLtlSpec_build has been invoked.

void Ltl_StructCheckLtlSpec_check

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Perform the check to see wether the property holds or not.

Perform the check to see wether the property holds or not. Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build.

If compassion is present it calls the check method for compassion, otherwise the check method dedicated to the algorithm given by the value of the oreg_justice_emptiness_bdd_algorithm option.

See also:

ltl_stuctcheckltlspec_check_compassion, ltl_structcheckltlspec_check_el_bwd, ltl_structcheckltlspec_check_el_fwd

Ltl_StructCheckLtlSpec_ptr Ltl_StructCheckLtlSpec_create	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop
	)			[related]

Create an empty Ltl_StructCheckLtlSpec structure.

void Ltl_StructCheckLtlSpec_destroy

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Desrtroy an Ltl_StructCheckLtlSpec structure.

void Ltl_StructCheckLtlSpec_explain	(	Ltl_StructCheckLtlSpec_ptr	self,
		NodeList_ptr	symbols
	)			[related]

Perform the computation of a witness for a property.

Perform the computation of a witness for a property. Assumes the Ltl_StructcCheckLtlSpec structure being initialized before with Ltl_StructCheckLtlSpec_build, and that Ltl_StructCheckLtlSpec_build has been invoked.

bdd_ptr Ltl_StructCheckLtlSpec_get_clean_s0

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Get the s0 field purified by tableu variables.

Get the s0 field of an Ltl_StructCheckLtlSpec structure purified by tableu variables

bdd_ptr Ltl_StructCheckLtlSpec_get_s0

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Get the s0 field of an Ltl_StructCheckLtlSpec structure.

Get the s0 field of an Ltl_StructCheckLtlSpec structure Returned bdd is NOT referenced.

void Ltl_StructCheckLtlSpec_print_result

(

Ltl_StructCheckLtlSpec_ptr

self

)

[related]

Prints the result of the Ltl_StructCheckLtlSpec_check fun.

Prints the result of the Ltl_StructCheckLtlSpec_check fun

void Ltl_StructCheckLtlSpec_set_do_rewriting	(	Ltl_StructCheckLtlSpec_ptr	self,
		boolean	do_rewriting
	)			[related]

Set the do_rewriting field of an Ltl_StructCheckLtlSpec structure.

Set the do_rewriting field of an Ltl_StructCheckLtlSpec structure

void Ltl_StructCheckLtlSpec_set_ltl2smv	(	Ltl_StructCheckLtlSpec_ptr	self,
		Ltl_StructCheckLtlSpec_ltl2smv	ltl2smv
	)			[related]

Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure.

Set the ltl2smv field of an Ltl_StructCheckLtlSpec structure

void Ltl_StructCheckLtlSpec_set_negate_formula	(	Ltl_StructCheckLtlSpec_ptr	self,
		boolean	negate_formula
	)			[related]

Set the negate_formula field of an Ltl_StructCheckLtlSpec structure.

Set the negate_formula field of an Ltl_StructCheckLtlSpec structure

void Ltl_StructCheckLtlSpec_set_oreg2smv	(	Ltl_StructCheckLtlSpec_ptr	self,
		Ltl_StructCheckLtlSpec_oreg2smv	oreg2smv
	)			[related]

Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure.

Set the oreg2smv field of an Ltl_StructCheckLtlSpec structure

---

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

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