Routines for working with a strategy, as a finite automaton. More...

#include <stdio.h>
#include "common.h"
#include "ptree.h"

Data Structures
struct	anode_t
	Strategy automaton nodes. More...

Macros
#define	DOT_AUT_ALL 0
	Show all variables with values.

#define	DOT_AUT_ATTRIB 4
	Show node attributes. More...

#define	DOT_AUT_BINARY 1
	Assume variables have Boolean domains, and only label nodes with those that are True.

#define	DOT_AUT_EDGEINPUT 2
	Show environment variables on edges.

Typedefs
typedef struct anode_t	anode_t
	Strategy automaton nodes.

Functions
int	anode_index (anode_t head, anode_t node)

anode_t *	append_anode_trans (anode_t head, int mode, vartype state, int state_len, int next_mode, vartype *next_state)

void	aut_aut_dump (anode_t head, int state_len, FILE fp)

int	aut_aut_dumpver (anode_t head, int state_len, FILE fp, int version)

anode_t *	aut_aut_load (int state_len, FILE *fp)

anode_t *	aut_aut_loadver (int state_len, FILE fp, int version)

int	aut_compact_nonbool (anode_t head, ptree_t evar_list, ptree_t svar_list, char name, int maxval)

int	aut_expand_bool (anode_t head, ptree_t evar_list, ptree_t svar_list, ptree_t nonbool_var_list)

anode_t *	aut_prune_deadends (anode_t *head)

int	aut_size (anode_t *head)

anode_t *	build_anode_trans (anode_t head, int mode, vartype state, int state_len, int next_mode, vartype **next_states, int next_len)

anode_t *	delete_anode (anode_t head, anode_t target)

void	delete_aut (anode_t *head)

int	dot_aut_dump (anode_t head, ptree_t evar_list, ptree_t svar_list, unsigned char format_flags, FILE fp)

anode_t *	find_anode (anode_t head, int mode, vartype state, int state_len)

int	find_anode_index (anode_t head, int mode, vartype state, int state_len)

int	forward_modereach (anode_t node, int mode, vartype *N, int N_len, int magic_mode, int state_len)

anode_t *	forward_prune (anode_t head, anode_t *U, int U_len)

anode_t *	insert_anode (anode_t head, int mode, int rgrad, bool initial, vartype state, int state_len)

int	json_aut_dump (anode_t head, ptree_t evar_list, ptree_t svar_list, FILE fp)

void	list_aut_dump (anode_t head, int state_len, FILE fp)

anode_t *	pop_anode (anode_t *head)

void	replace_anode_trans (anode_t head, anode_t old, anode_t *new)

int	spin_aut_dump (anode_t head, ptree_t evar_list, ptree_t svar_list, ptree_t env_init, ptree_t sys_init, ptree_t env_trans_array, int et_array_len, ptree_t sys_trans_array, int st_array_len, ptree_t env_goals, int num_env_goals, ptree_t sys_goals, int num_sys_goals, FILE fp)

int	tulip0_aut_dump (anode_t head, ptree_t evar_list, ptree_t svar_list, FILE fp)

int	tulip_aut_dump (anode_t head, ptree_t evar_list, ptree_t svar_list, FILE fp)

Detailed Description

Routines for working with a strategy, as a finite automaton.

Note that the length of the state vector in each node is not stored anywhere in this data structure. It is assumed to be positive and constant for a particular automaton (strategy).

SCL; 2012-2015

Function Documentation

int anode_index	(	anode_t *	head,
		anode_t *	node
	)

Return the position of the given node, or -1 if not found. 0-based indexing.

anode_t* append_anode_trans	(	anode_t *	head,
		int	mode,
		vartype *	state,
		int	state_len,
		int	next_mode,
		vartype *	next_state
	)

Append transition to array for the first node with given state and mode. Return new head on success, NULL on error.

void aut_aut_dump	(	anode_t *	head,
		int	state_len,
		FILE *	fp
	)

Dump strategy using the current version of the "gr1c automaton" file format. Read external_notes for details. If fp = NULL, then write to stdout.

int aut_aut_dumpver	(	anode_t *	head,
		int	state_len,
		FILE *	fp,
		int	version
	)

Dump strategy using the specified version of the "gr1c automaton" file format. This function is wrapped by aut_aut_dump(). Return 0 on success. If the given version number is not supported, then return -1.

anode_t* aut_aut_load	(	int	state_len,
		FILE *	fp
	)

Legacy wrapper for aut_aut_load(). Equivalent to calling aut_aut_loadver() with version == NULL

anode_t* aut_aut_loadver	(	int	state_len,
		FILE *	fp,
		int *	version
	)

Load strategy given in "gr1c automaton" format from file fp. Read external_notes for details. If fp = NULL, then read from stdin. Return resulting head pointer, or NULL if error. If version is not NULL, then the detected format version number is placed in *version.

Note that attempting to load a gr1c automaton file for a version that includes fields not present in this build of gr1c results in a warning message while all supported fields are used. If expected fields are missing (e.g., no rgrad number is available), then the appropriate "unset" indicator is set to each such field; typically this is -1, check the definition of anode_t for details.

int aut_compact_nonbool	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		char *	name,
		int	maxval
	)

Convert binary-expanded form of a variable back into nonboolean. The domain of the variable is [0,maxval], and to indicate this the value field is set to maxval in the resulting (merged) variable entry (in evar_list or svar_list). Returns the new state vector length, or -1 on error.

int aut_expand_bool	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		ptree_t *	nonbool_var_list
	)

Inverse operation of aut_compact_nonbool(). Return zero on success, nonzero on error.

anode_t* aut_prune_deadends ( anode_t * head )

Return (possibly new) head pointer.

int aut_size ( anode_t * head )

Get number of nodes in given automaton.

anode_t* build_anode_trans	(	anode_t *	head,
		int	mode,
		vartype *	state,
		int	state_len,
		int	next_mode,
		vartype **	next_states,
		int	next_len
	)

Build the transition array for the first node with given state and mode.

next_states is an array of state vectors, with length next_len, used to build transitions for this node. All of these states have mode next_mode, and the actual transitions are to the first nodes found with these states and mode.

If the base node already has a transition array, then it is not replaced until the new array has been successfully built. (That is, if error, the original node should be unaffected.)

Return given head on success, NULL if one of the needed nodes is not found.

anode_t* delete_anode	(	anode_t *	head,
		anode_t *	target
	)

Return (possibly new) head pointer. Transition arrays are not altered by this function.

void delete_aut ( anode_t * head )

Delete entire automaton pointed to by given head.

Essentially, traverses node list and frees them and their member data. At completion, the given head pointer is no longer valid. Invoking with NULL pointer causes return with no error.

int dot_aut_dump	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		unsigned char	format_flags,
		FILE *	fp
	)

Dump DOT file describing the automaton (strategy). The appearance can be configured using format flags for dot_aut_dump. Also read comments for tulip_aut_dump().

anode_t* find_anode	(	anode_t *	head,
		int	mode,
		vartype *	state,
		int	state_len
	)

Return pointer to the first node with given state and mode, or NULL if not found.

int find_anode_index	(	anode_t *	head,
		int	mode,
		vartype *	state,
		int	state_len
	)

Return the position of the first node with given state and mode, or -1 if not found. 0-based indexing.

int forward_modereach	(	anode_t *	node,
		int	mode,
		vartype **	N,
		int	N_len,
		int	magic_mode,
		int	state_len
	)

Compute forward reachable set from given node in automaton, restricting attention to nodes with state in N and goal mode of mode, and setting the mode field of each reached node to magic_mode. Return zero on success, nonzero on error.

anode_t* forward_prune	(	anode_t *	head,
		anode_t **	U,
		int	U_len
	)

Delete nodes in U that are not reachable in the graph from outside U, and then repeat. Nodes marked as initial are ignored; such nodes are supposed to satisfy initial conditions, i.e., from which execution is allowed to begin and hence do not need ingoing edges.

The given array U is altered and freed during execution of forward_prune(), so the caller should not attempt to use it afterward.

U may be redundant, i.e., the implementation is tolerant to U having multiple pointers to the same node.

Return (possibly new) head pointer, or NULL on error.

anode_t* insert_anode	(	anode_t *	head,
		int	mode,
		int	rgrad,
		bool	initial,
		vartype *	state,
		int	state_len
	)

Insert node at the front of the given node list. If given head is NULL, a new list will be created.

Return new head on success, NULL on error.

int json_aut_dump	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		FILE *	fp
	)

Dump strategy using the current version of the gr1c-JSON file format. Consult external_notes for details.

void list_aut_dump	(	anode_t *	head,
		int	state_len,
		FILE *	fp
	)

Dump list of nodes; mostly useful for debugging. If fp = NULL, then write to stdout. The basic format is

i [(init)] : S - m - r - [t0 t1 ...]

where i is the node ID (used only as a means to uniquely refer to nodes), S is the state at that node as comma-separated values, m is the goal mode, r is the reach annotation value, and [t0 t1 ...] is the list of IDs of nodes reachable in one step. The node ID is followed by "(init)" if the initial field is marked True.

anode_t* pop_anode ( anode_t * head )

Delete topmost (head) node from list. Return pointer to new head.

void replace_anode_trans	(	anode_t *	head,
		anode_t *	old,
		anode_t *	new
	)

Replace all occurrences of "old" with "new" in transition arrays. If "new" is NULL, then the transitions into "old" are deleted and all dependent transition array lengths are decremented.

int spin_aut_dump	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		ptree_t *	env_init,
		ptree_t *	sys_init,
		ptree_t **	env_trans_array,
		int	et_array_len,
		ptree_t **	sys_trans_array,
		int	st_array_len,
		ptree_t **	env_goals,
		int	num_env_goals,
		ptree_t **	sys_goals,
		int	num_sys_goals,
		FILE *	fp
	)

Dump strategy as Spin Promela model.

Assumptions:

no more than 10000 environment goals;
no more than 10000 system goals;
none of the variables has the following names: checketrans, checkstrans, pmlfault, envinit, envtrans, envgoal0, envgoal1, ... sysinit, systrans, sysgoal0, sysgoal1, ...

If fp = NULL, then write to stdout. Return nonzero if error.

int tulip0_aut_dump	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		FILE *	fp
	)

Dump using tulipcon version 0. DEPRECATED! Please use tulip_aut_dump() instead. tulip0_aut_dump() is provided only for legacy code and will soon be removed.

int tulip_aut_dump	(	anode_t *	head,
		ptree_t *	evar_list,
		ptree_t *	svar_list,
		FILE *	fp
	)

Dump tulipcon XML file describing the automaton (strategy). Variable names are obtained from evar_list and svar_list, in which the combined order is assumed to match that of the state vector in each automaton node.

For each node, the goal mode and reach annotation value are placed in a <anno> tag in that order.

If fp = NULL, then write to stdout. Return nonzero if error.

Data Structures

Macros

Typedefs

Functions

Detailed Description

Function Documentation