gr1c
0.12.0
|
Routines for working with a strategy, as a finite automaton. More...
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, FILE *formula_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) |
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
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.
This function does not check for duplicate outgoing edges.
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.
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.
Delete target node from strategy automaton.
Note that any references to target
in transition arrays of other nodes are not modified by this function. If you want to change or delete any such pointers to target
, use replace_anode_trans().
head | pointer to the strategy automaton to be modified. |
target | node to be deleted. The associated state vector and transition array are freed. If target is not found, then return value is NULL. |
head
or target
is NULL or if target
is not found, then return NULL. If head=target and there is only one node, then return NULL (because the only node is deleted, there can be no head pointer). 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().
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.
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.
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.
Delete topmost (head) node from list. Return pointer to new head.
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, | ||
FILE * | formula_fp | ||
) |
Dump strategy as Spin Promela model.
Assumptions:
An LTL formula that can be used to decide whether the strategy realizes the GR(1) specification is included in the comments near the top of the generated Spin Promela model.
Example instructions for model checking are provided in doc/verification.md.
If fp = NULL, then write to stdout.
If fp != NULL, then formula_fp is the file in which to print the LTL formula, or stdout if formula_fp = NULL. Note that this is a copy of the LTL formula that is included in the Promela model, which is described above.
If fp = formula_fp (i.e., the same file pointer), then do not print the LTL formula to formula_fp.
Return nonzero if error.
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.
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.