Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
divine-ltsmin-deb
Commits
35cc50f0
Commit
35cc50f0
authored
Sep 22, 2014
by
Jeroen Meijer
Browse files
add actions read matrix
parent
94c0b1ce
Changes
2
Expand all
Hide whitespace changes
Inline
Side-by-side
tools/dvecompile.cpp
View file @
35cc50f0
This diff is collapsed.
Click to expand it.
tools/dvecompile.h
View file @
35cc50f0
...
...
@@ -23,6 +23,7 @@ struct ext_transition_t
std
::
vector
<
int
>
sv_read
;
std
::
vector
<
int
>
sv_may_write
;
std
::
vector
<
int
>
sv_must_write
;
std
::
vector
<
int
>
sv_actions_read
;
};
typedef
enum
{
GUARD_EXPR
,
GUARD_PC
,
GUARD_CHAN
,
GUARD_COMMITED_FIRST
}
guard_type
;
...
...
@@ -107,7 +108,7 @@ struct dve_compiler: public dve_explicit_system_t
int
count_state_variables
();
void
analyse_expression
(
dve_expression_t
&
expr
,
ext_transition_t
&
ext_transition
,
std
::
vector
<
int
>
&
dep
);
void
output_dependency_comment
(
ext_transition_t
&
ext_transition
);
void
output_dependency_comment
(
ext_transition_t
&
ext_transition
,
bool
condition
);
void
mark_dependency
(
size_int_t
gid
,
int
type
,
int
idx
,
std
::
vector
<
int
>
&
dep
);
void
analyse_transition_dependencies
(
ext_transition_t
&
ext_transition
);
void
analyse_transition
(
dve_transition_t
*
transition
,
...
...
@@ -229,7 +230,7 @@ struct dve_compiler: public dve_explicit_system_t
void
new_output_state
();
void
gen_successors
();
void
gen_ltsmin_successors
();
void
gen_ltsmin_successors
(
bool
condition
);
void
gen_is_accepting
();
void
gen_header
();
void
gen_state_struct
();
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment