#include "nusmv/core/dd/dd.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/array.h"#include "nusmv/core/utils/error.h"#include "nusmv/core/trace/plugins/TracePlugin.h"#include "nusmv/core/trace/exec/PartialTraceExecutor.h"#include "nusmv/core/trace/exec/CompleteTraceExecutor.h"#include "nusmv/core/trace/eval/BaseEvaluator.h"#include "nusmv/core/trace/TraceLabel.h"#include "nusmv/core/trace/TraceOpt.h"#include "nusmv/core/node/node.h"Go to the source code of this file.
Defines | |
| #define | ENV_TRACE_COMPACT "env_trace_compact" |
| #define | ENV_TRACE_EMBEDDED_XML_DUMPER "env_trace_embedded_xml_dumper" |
| #define | ENV_TRACE_EMPTY_INDEX "etraceemptyindex" |
| #define | ENV_TRACE_EXPLAINER "env_trace_explainer" |
| #define | ENV_TRACE_EXPLAINER_CHANGES_ONLY "env_trace_explainer_changes_only" |
| Environment handles for trace plugins. | |
| #define | ENV_TRACE_TABLE_COLUMN "env_trace_table_column" |
| #define | ENV_TRACE_TABLE_ROW "env_trace_table_row" |
| #define | ENV_TRACE_XML_DUMPER "env_trace_xml_dumper" |
| #define | TRACE_MGR(x) ((TraceMgr_ptr) x) |
| #define | TRACE_MGR_CHECK_INSTANCE(x) (nusmv_assert(TRACE_MGR(x) != TRACE_MGR(NULL))) |
| #define | TRACE_MGR_DEFAULT_PLUGIN -1 |
The header file for the TraceMgr class. | |
| #define | TRACE_MGR_LAST_TRACE -1 |
Typedefs | |
| typedef struct TraceMgr_TAG * | TraceMgr_ptr |
Functions | |
| int | TraceMgr_execute_partial_traces (TraceMgr_ptr const self, PartialTraceExecutor_ptr const executor, const int first_trace, const int last_trace) |
| Executes partial traces on the model FSM. | |
| int | TraceMgr_execute_traces (TraceMgr_ptr const self, CompleteTraceExecutor_ptr const executor, const int first_trace, const int last_trace) |
| Executes complete traces on the model FSM. | |
| CompleteTraceExecutor_ptr | TraceMgr_get_default_complete_trace_executor (const TraceMgr_ptr global_trace_manager) |
| Returns default registered complete trace executor. | |
| PartialTraceExecutor_ptr | TraceMgr_get_default_partial_trace_executor (const TraceMgr_ptr global_trace_manager) |
| Returns default registered partial trace executor. | |
| int | TraceMgr_show_plugins (TraceMgr_ptr const self, const boolean is_show_all, const int dp) |
| int | TraceMgr_show_traces (TraceMgr_ptr const self, const int plugin_index, const boolean is_all, const int trace, TraceOpt_ptr const trace_opt, const int traceno, int from_state, int to_state) |
| Shows the traces generated in a NuSMV session. | |
| #define ENV_TRACE_EMBEDDED_XML_DUMPER "env_trace_embedded_xml_dumper" |
| #define ENV_TRACE_EXPLAINER_CHANGES_ONLY "env_trace_explainer_changes_only" |
Environment handles for trace plugins.
Environment handles to retrieve the right index of a trace plugin, thus avoiding to use magic numbers.
WARNING: The indexes retrieved from the environment with these handles have to be lowered of one. This is necessary because a plugin can have a 0 index, that clashes with the pointer NULL value
required
| #define ENV_TRACE_TABLE_COLUMN "env_trace_table_column" |
| #define TRACE_MGR | ( | x | ) | ((TraceMgr_ptr) x) |
| #define TRACE_MGR_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(TRACE_MGR(x) != TRACE_MGR(NULL))) |
| #define TRACE_MGR_DEFAULT_PLUGIN -1 |
| typedef struct TraceMgr_TAG* TraceMgr_ptr |
| int TraceMgr_execute_partial_traces | ( | TraceMgr_ptr const | self, | |
| PartialTraceExecutor_ptr const | executor, | |||
| const int | first_trace, | |||
| const int | last_trace | |||
| ) |
Executes partial traces on the model FSM.
Execute the traces between first trace and last trace
| int TraceMgr_execute_traces | ( | TraceMgr_ptr const | self, | |
| CompleteTraceExecutor_ptr const | executor, | |||
| const int | first_trace, | |||
| const int | last_trace | |||
| ) |
Executes complete traces on the model FSM.
Execute the traces between first trace and last trace
| CompleteTraceExecutor_ptr TraceMgr_get_default_complete_trace_executor | ( | const TraceMgr_ptr | global_trace_manager | ) |
Returns default registered complete trace executor.
Returns default registered complete trace executor, if any. If no executor has yet been registered NULL is returned.
TODO[MP] default policy must be revised now it's lexicographic order
none
| PartialTraceExecutor_ptr TraceMgr_get_default_partial_trace_executor | ( | const TraceMgr_ptr | global_trace_manager | ) |
Returns default registered partial trace executor.
Returns default registered partial trace executor, if any. If no executor has yet been registered NULL is returned.
TODO[MP] default policy must be revised now it's lexicographic order
none
| int TraceMgr_show_plugins | ( | TraceMgr_ptr const | self, | |
| const boolean | is_show_all, | |||
| const int | dp | |||
| ) |
Lists out all the available plugins inside the system.
| int TraceMgr_show_traces | ( | TraceMgr_ptr const | self, | |
| const int | plugin_index, | |||
| const boolean | is_all, | |||
| const int | trace, | |||
| TraceOpt_ptr const | trace_opt, | |||
| const int | traceno, | |||
| int | from_state, | |||
| int | to_state | |||
| ) |
Shows the traces generated in a NuSMV session.
Shows the traces generated in a NuSMV session
1.6.1