NuSMV/code/nusmv/core/parser/psl/pslExpr.h File Reference

#include "nusmv/core/parser/psl/pslNode.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/error.h"

Go to the source code of this file.

Data Structures
struct	PslExpr
Defines
#define	PSL_EXPR_MAKE_B2B_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_B2F_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_FL_PROPERTY)
#define	PSL_EXPR_MAKE_B2W_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_WORD_EXPR)
#define	PSL_EXPR_MAKE_B_B2B_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_BOOL_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_B_B2F_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_BOOL_EXPR, SC_FL_PROPERTY)
#define	PSL_EXPR_MAKE_BW2BW_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_WORD_EXPR, SC_BOOL_WORD_EXPR)
#define	PSL_EXPR_MAKE_BW_BW2BW_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_EXT_NEXT_OP_BOOL(env, res, operator, fl_property, bool_expr)   psl_expr_make_extended_next_op(env, operator, &fl_property, NULL, &bool_expr, &res);
#define	PSL_EXPR_MAKE_EXT_NEXT_OP_WHEN(env, res, operator, fl_property, when)   psl_expr_make_extended_next_op(env, operator, &fl_property, &when, NULL, &res);
#define	PSL_EXPR_MAKE_EXT_NEXT_OP_WHEN_BOOL(env, res, operator, fl_property, when, bool_expr)   psl_expr_make_extended_next_op(env, operator, &fl_property, &when, &bool_expr, &res);
#define	PSL_EXPR_MAKE_F2F_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_FL_PROPERTY, SC_FL_PROPERTY)
#define	PSL_EXPR_MAKE_F_F2F_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_FL_PROPERTY, SC_FL_PROPERTY)
#define	PSL_EXPR_MAKE_N2B_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_N2N_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_EXPR, SC_NUM_EXPR)
#define	PSL_EXPR_MAKE_N_N2B_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_N_N2N_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_EXPR, SC_NUM_EXPR)
#define	PSL_EXPR_MAKE_N_N2W_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_N_W2W_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_NB_NB2B_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_NB_NB2N_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_EXPR, SC_NUM_EXPR)
#define	PSL_EXPR_MAKE_NBW2B_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_BOOL_WORD_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_NBW2N_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_BOOL_WORD_EXPR, SC_NUM_EXPR)
#define	PSL_EXPR_MAKE_NBW_NBW2B_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_WORD_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_NBW_NBW2N_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_WORD_EXPR, SC_NUM_EXPR)
#define	PSL_EXPR_MAKE_NW2NW_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_WORD_EXPR, SC_NUM_WORD_EXPR)
#define	PSL_EXPR_MAKE_NW_NW2B_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_WORD_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_NW_NW2NW_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_WORD_EXPR, SC_NUM_WORD_EXPR)
#define	PSL_EXPR_MAKE_T2T_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, right.klass, right.klass)
#define	PSL_EXPR_MAKE_T_T2T_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, left.klass, left.klass)
#define	PSL_EXPR_MAKE_W2B_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_W2N_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_BOOL_EXPR)
#define	PSL_EXPR_MAKE_W2W_OP(env, res, right, op)   psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_WORD_EXPR)
#define	PSL_EXPR_MAKE_W_N2W_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_W_N2W_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_W_NW2W_OP(env, res, left, op, right)
#define	PSL_EXPR_MAKE_W_W2W_OP(env, res, left, op, right)   psl_expr_make_binary_op(env, &res, &left, op, &right, SC_WORD_EXPR, SC_WORD_EXPR)
Enumerations
enum	SyntaxClass {   SC_NUM_EXPR, SC_BOOL_EXPR, SC_WORD_EXPR, SC_IDENTIFIER,   SC_NUM_BOOL_WORD_EXPR, SC_NUM_BOOL_EXPR, SC_BOOL_WORD_EXPR, SC_NUM_WORD_EXPR,   SC_PROPERTY, SC_FL_PROPERTY, SC_OBE_PROPERTY, SC_SEQUENCE,   SC_REPLICATOR, SC_NONE, SC_RANGE, SC_LIST,   SC_NUM_RANGE }
	PSL parser interface. More...
Functions
PslExpr	psl_expr_make_abort (const NuSMVEnv_ptr env, PslExpr fl_prop, PslExpr cond)
PslExpr	psl_expr_make_atom (const NuSMVEnv_ptr env, const char *str)
PslExpr	psl_expr_make_base_number (const NuSMVEnv_ptr env, char *base_num)
void	psl_expr_make_binary_mixed_op (const NuSMVEnv_ptr env, PslExpr *res, const PslExpr *left, const PslOp op_id, const PslExpr *right, const SyntaxClass left_req_klass, const SyntaxClass right_req_klass, const SyntaxClass res_klass)
void	psl_expr_make_binary_op (const NuSMVEnv_ptr env, PslExpr *res, const PslExpr *left, const PslOp op_id, const PslExpr *right, const SyntaxClass ops_req_klass, const SyntaxClass res_klass)
PslExpr	psl_expr_make_bit_selection (const NuSMVEnv_ptr env, PslExpr word_expr, PslExpr left, PslExpr right)
PslExpr	psl_expr_make_boolean_type (const NuSMVEnv_ptr env)
PslExpr	psl_expr_make_boolean_value (const NuSMVEnv_ptr env, int val)
PslExpr	psl_expr_make_case (const NuSMVEnv_ptr env, PslExpr cond, PslExpr _then, PslExpr _list)
PslExpr	psl_expr_make_concatenation (const NuSMVEnv_ptr env, PslExpr expr_list)
PslExpr	psl_expr_make_cons (const NuSMVEnv_ptr env, PslExpr a, PslExpr b)
PslExpr	psl_expr_make_cons_new (const NuSMVEnv_ptr env, PslExpr a, PslExpr b)
PslExpr	psl_expr_make_context (const NuSMVEnv_ptr env, PslExpr ctx, PslExpr node)
PslExpr	psl_expr_make_empty (void)
void	psl_expr_make_extended_next_op (const NuSMVEnv_ptr env, PslOp op_id, const PslExpr *fl_property, const PslExpr *when, const PslExpr *bool_expr, PslExpr *res)
PslExpr	psl_expr_make_failure (const NuSMVEnv_ptr env, const char *msg, FailureKind kind)
PslExpr	psl_expr_make_false (const NuSMVEnv_ptr env)
PslExpr	psl_expr_make_id (const NuSMVEnv_ptr env, PslExpr left, PslExpr right)
PslExpr	psl_expr_make_id_array (const NuSMVEnv_ptr env, PslExpr id, PslExpr num)
PslExpr	psl_expr_make_inf (const NuSMVEnv_ptr env)
PslExpr	psl_expr_make_ite (const NuSMVEnv_ptr env, PslExpr cond, PslExpr _then, PslExpr _else)
PslExpr	psl_expr_make_multiple_concatenation (const NuSMVEnv_ptr env, PslExpr expr, PslExpr expr_list)
PslExpr	psl_expr_make_number (const NuSMVEnv_ptr env, int val)
PslExpr	psl_expr_make_obe_binary (const NuSMVEnv_ptr env, PslExpr left, PslOp op, PslExpr right)
PslExpr	psl_expr_make_obe_unary (const NuSMVEnv_ptr env, PslOp op, PslExpr expr)
PslExpr	psl_expr_make_range (const NuSMVEnv_ptr env, PslExpr low, PslExpr high)
PslExpr	psl_expr_make_real_number (const NuSMVEnv_ptr env, char *fval)
PslExpr	psl_expr_make_repeated_sere (const NuSMVEnv_ptr env, PslOp op, PslExpr sere, PslExpr count)
PslExpr	psl_expr_make_replicated_property (const NuSMVEnv_ptr env, PslExpr replicator, PslExpr expr)
PslExpr	psl_expr_make_replicator (const NuSMVEnv_ptr env, PslOp op_id, PslExpr id, PslExpr range, PslExpr value_set)
PslExpr	psl_expr_make_sere (const NuSMVEnv_ptr env, PslExpr expr)
PslExpr	psl_expr_make_sere_compound_binary_op (const NuSMVEnv_ptr env, PslExpr seq1, PslOp op, PslExpr seq2)
PslExpr	psl_expr_make_sere_concat (const NuSMVEnv_ptr env, PslExpr seq1, PslExpr seq2)
PslExpr	psl_expr_make_sere_fusion (const NuSMVEnv_ptr env, PslExpr seq1, PslExpr seq2)
PslExpr	psl_expr_make_suffix_implication_strong (const NuSMVEnv_ptr env, PslExpr seq, PslOp op, PslExpr expr)
PslExpr	psl_expr_make_suffix_implication_weak (const NuSMVEnv_ptr env, PslExpr seq, PslOp op, PslExpr expr)
PslExpr	psl_expr_make_true (const NuSMVEnv_ptr env)
void	psl_expr_make_unary_op (const NuSMVEnv_ptr env, PslExpr *res, const PslExpr *right, const PslOp op_id, const SyntaxClass right_req_klass, const SyntaxClass res_klass)
PslExpr	psl_expr_make_whilenot (const NuSMVEnv_ptr env, PslOp op, PslExpr expr, PslExpr seq)
PslExpr	psl_expr_make_within (const NuSMVEnv_ptr env, PslOp op, PslExpr begin, PslExpr end, PslExpr seq)
PslExpr	psl_expr_make_word_concatenation (const NuSMVEnv_ptr env, PslExpr left, PslExpr right)
PslExpr	psl_expr_make_word_number (const NuSMVEnv_ptr env, char *wval)

---

Define Documentation

#define PSL_EXPR_MAKE_B2B_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_B2F_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_FL_PROPERTY)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_B2W_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_B_B2B_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_BOOL_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_B_B2F_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_BOOL_EXPR, SC_FL_PROPERTY)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_BW2BW_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_BOOL_WORD_EXPR, SC_BOOL_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_BW_BW2BW_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_op(env, &res, &left, op, &right,              \
                          SC_BOOL_WORD_EXPR, SC_BOOL_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_EXT_NEXT_OP_BOOL	(	env,
		res,
		operator,
		fl_property,
		bool_expr		)	psl_expr_make_extended_next_op(env, operator, &fl_property, NULL, &bool_expr, &res);

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_EXT_NEXT_OP_WHEN	(	env,
		res,
		operator,
		fl_property,
		when		)	psl_expr_make_extended_next_op(env, operator, &fl_property, &when, NULL, &res);

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_EXT_NEXT_OP_WHEN_BOOL	(	env,
		res,
		operator,
		fl_property,
		when,
		bool_expr		)	psl_expr_make_extended_next_op(env, operator, &fl_property, &when, &bool_expr, &res);

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_F2F_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_FL_PROPERTY, SC_FL_PROPERTY)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_F_F2F_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_FL_PROPERTY, SC_FL_PROPERTY)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N2B_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N2N_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_EXPR, SC_NUM_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N_N2B_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N_N2N_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_EXPR, SC_NUM_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N_N2W_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_op(env, &res, &left, op, &right,      \
                          SC_NUM_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_N_W2W_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_mixed_op(env, &res, &left, op, &right,                \
                                SC_NUM_EXPR, SC_WORD_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NB_NB2B_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NB_NB2N_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_EXPR, SC_NUM_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NBW2B_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_BOOL_WORD_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NBW2N_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_BOOL_WORD_EXPR, SC_NUM_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NBW_NBW2B_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_WORD_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NBW_NBW2N_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_BOOL_WORD_EXPR, SC_NUM_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NW2NW_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_NUM_WORD_EXPR, SC_NUM_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NW_NW2B_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_WORD_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_NW_NW2NW_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_NUM_WORD_EXPR, SC_NUM_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_T2T_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, right.klass, right.klass)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_T_T2T_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, left.klass, left.klass)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W2B_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W2N_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_BOOL_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W2W_OP	(	env,
		res,
		right,
		op		)	psl_expr_make_unary_op(env, &res, &right, op, SC_WORD_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W_N2W_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_mixed_op(env, &res, &left, op, &right,                \
                                SC_WORD_EXPR, SC_NUM_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W_N2W_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_mixed_op(env, &res, &left, op, &right,                \
                                SC_WORD_EXPR, SC_NUM_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W_NW2W_OP	(	env,
		res,
		left,
		op,
		right		)

Value:

psl_expr_make_binary_mixed_op(env, &res, &left, op, &right,                \
                                SC_WORD_EXPR, SC_NUM_WORD_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

#define PSL_EXPR_MAKE_W_W2W_OP	(	env,
		res,
		left,
		op,
		right		)	psl_expr_make_binary_op(env, &res, &left, op, &right, SC_WORD_EXPR, SC_WORD_EXPR)

Todo:

Missing synopsis

Todo:

Missing description

---

Enumeration Type Documentation

enum SyntaxClass

PSL parser interface.

Author:

Roberto Cavada

Todo:

: Missing description

Enumerator:

SC_NUM_EXPR
SC_BOOL_EXPR
SC_WORD_EXPR
SC_IDENTIFIER
SC_NUM_BOOL_WORD_EXPR
SC_NUM_BOOL_EXPR
SC_BOOL_WORD_EXPR
SC_NUM_WORD_EXPR
SC_PROPERTY
SC_FL_PROPERTY
SC_OBE_PROPERTY
SC_SEQUENCE
SC_REPLICATOR
SC_NONE
SC_RANGE
SC_LIST
SC_NUM_RANGE

---

Function Documentation

PslExpr psl_expr_make_abort	(	const NuSMVEnv_ptr	env,
		PslExpr	fl_prop,
		PslExpr	cond
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_atom	(	const NuSMVEnv_ptr	env,
		const char *	str
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_base_number	(	const NuSMVEnv_ptr	env,
		char *	base_num
	)

Todo:

Missing synopsis

Todo:

Missing description

void psl_expr_make_binary_mixed_op	(	const NuSMVEnv_ptr	env,
		PslExpr *	res,
		const PslExpr *	left,
		const PslOp	op_id,
		const PslExpr *	right,
		const SyntaxClass	left_req_klass,
		const SyntaxClass	right_req_klass,
		const SyntaxClass	res_klass
	)

Todo:

Missing synopsis

Todo:

Missing description

void psl_expr_make_binary_op	(	const NuSMVEnv_ptr	env,
		PslExpr *	res,
		const PslExpr *	left,
		const PslOp	op_id,
		const PslExpr *	right,
		const SyntaxClass	ops_req_klass,
		const SyntaxClass	res_klass
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_bit_selection	(	const NuSMVEnv_ptr	env,
		PslExpr	word_expr,
		PslExpr	left,
		PslExpr	right
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_boolean_type

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_boolean_value	(	const NuSMVEnv_ptr	env,
		int	val
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_case	(	const NuSMVEnv_ptr	env,
		PslExpr	cond,
		PslExpr	_then,
		PslExpr	_list
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_concatenation	(	const NuSMVEnv_ptr	env,
		PslExpr	expr_list
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_cons	(	const NuSMVEnv_ptr	env,
		PslExpr	a,
		PslExpr	b
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_cons_new	(	const NuSMVEnv_ptr	env,
		PslExpr	a,
		PslExpr	b
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_context	(	const NuSMVEnv_ptr	env,
		PslExpr	ctx,
		PslExpr	node
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_empty

(

void

)

Todo:

Missing synopsis

Todo:

Missing description

void psl_expr_make_extended_next_op	(	const NuSMVEnv_ptr	env,
		PslOp	op_id,
		const PslExpr *	fl_property,
		const PslExpr *	when,
		const PslExpr *	bool_expr,
		PslExpr *	res
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_failure	(	const NuSMVEnv_ptr	env,
		const char *	msg,
		FailureKind	kind
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_false

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_id	(	const NuSMVEnv_ptr	env,
		PslExpr	left,
		PslExpr	right
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_id_array	(	const NuSMVEnv_ptr	env,
		PslExpr	id,
		PslExpr	num
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_inf

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_ite	(	const NuSMVEnv_ptr	env,
		PslExpr	cond,
		PslExpr	_then,
		PslExpr	_else
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_multiple_concatenation	(	const NuSMVEnv_ptr	env,
		PslExpr	expr,
		PslExpr	expr_list
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_number	(	const NuSMVEnv_ptr	env,
		int	val
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_obe_binary	(	const NuSMVEnv_ptr	env,
		PslExpr	left,
		PslOp	op,
		PslExpr	right
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_obe_unary	(	const NuSMVEnv_ptr	env,
		PslOp	op,
		PslExpr	expr
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_range	(	const NuSMVEnv_ptr	env,
		PslExpr	low,
		PslExpr	high
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_real_number	(	const NuSMVEnv_ptr	env,
		char *	fval
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_repeated_sere	(	const NuSMVEnv_ptr	env,
		PslOp	op,
		PslExpr	sere,
		PslExpr	count
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_replicated_property	(	const NuSMVEnv_ptr	env,
		PslExpr	replicator,
		PslExpr	expr
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_replicator	(	const NuSMVEnv_ptr	env,
		PslOp	op_id,
		PslExpr	id,
		PslExpr	range,
		PslExpr	value_set
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_sere	(	const NuSMVEnv_ptr	env,
		PslExpr	expr
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_sere_compound_binary_op	(	const NuSMVEnv_ptr	env,
		PslExpr	seq1,
		PslOp	op,
		PslExpr	seq2
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_sere_concat	(	const NuSMVEnv_ptr	env,
		PslExpr	seq1,
		PslExpr	seq2
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_sere_fusion	(	const NuSMVEnv_ptr	env,
		PslExpr	seq1,
		PslExpr	seq2
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_suffix_implication_strong	(	const NuSMVEnv_ptr	env,
		PslExpr	seq,
		PslOp	op,
		PslExpr	expr
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_suffix_implication_weak	(	const NuSMVEnv_ptr	env,
		PslExpr	seq,
		PslOp	op,
		PslExpr	expr
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_true

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

void psl_expr_make_unary_op	(	const NuSMVEnv_ptr	env,
		PslExpr *	res,
		const PslExpr *	right,
		const PslOp	op_id,
		const SyntaxClass	right_req_klass,
		const SyntaxClass	res_klass
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_whilenot	(	const NuSMVEnv_ptr	env,
		PslOp	op,
		PslExpr	expr,
		PslExpr	seq
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_within	(	const NuSMVEnv_ptr	env,
		PslOp	op,
		PslExpr	begin,
		PslExpr	end,
		PslExpr	seq
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_word_concatenation	(	const NuSMVEnv_ptr	env,
		PslExpr	left,
		PslExpr	right
	)

Todo:

Missing synopsis

Todo:

Missing description

PslExpr psl_expr_make_word_number	(	const NuSMVEnv_ptr	env,
		char *	wval
	)

Todo:

Missing synopsis

Todo:

Missing description