Skip to content
GitLab
Menu
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
d1b974aa
Commit
d1b974aa
authored
Aug 06, 2010
by
Elwin Pater
Committed by
Michael Weber
Nov 05, 2010
Browse files
Added simple guard co-enabled matrix
parent
c218c737
Changes
2
Hide whitespace changes
Inline
Side-by-side
tools/dvecompile.cpp
View file @
d1b974aa
...
...
@@ -2194,8 +2194,78 @@ void dve_compiler::gen_transition_info()
line
(
buf
);
block_end
();
line
();
//////////////////////////////////////////
// EXPORT GUARD MAY BE COENABLED MATRIX //
//////////////////////////////////////////
// guard may be co-enabled matrix (#guards x #guards)
sprintf
(
buf
,
"int guardmaybecoenabled[%zu][%zu] = "
,
guard
.
size
(),
guard
.
size
());
line
(
buf
);
block_begin
();
for
(
size_int_t
i
=
0
;
i
<
guard
.
size
();
i
++
)
{
append
(
"{"
);
for
(
size_int_t
j
=
0
;
j
<
guard
.
size
();
j
++
)
{
if
(
j
!=
0
)
append
(
", "
);
if
(
may_be_coenabled
(
guard
[
i
],
guard
[
j
]))
{
append
(
"1"
);
}
else
{
append
(
"0"
);
}
}
if
(
i
==
guard
.
size
()
-
1
)
line
(
"}"
);
else
line
(
"},"
);
}
block_end
();
line
(
";"
);
line
();
// may be co-enabled function
line
(
"extern
\"
C
\"
const int* get_guards_may_be_coenabled_matrix(int g) "
);
block_begin
();
sprintf
(
buf
,
"if (g>=0 && g < %zu) return guardmaybecoenabled[g];"
,
guard
.
size
());
line
(
buf
);
sprintf
(
buf
,
"return NULL;"
);
line
(
buf
);
block_end
();
line
();
}
bool
dve_compiler
::
may_be_coenabled
(
guard
&
ga
,
guard
&
gb
)
{
// if type different, return default
if
(
ga
.
type
==
gb
.
type
||
ga
.
type
==
GUARD_COMMITED_FIRST
)
{
switch
(
ga
.
type
)
{
case
GUARD_PC
:
// if one committed, and the other is not, they may not be co-enabled
if
(
dynamic_cast
<
dve_process_t
*>
(
get_process
(
ga
.
pc
.
gid
))
->
get_commited
(
ga
.
pc
.
lid
)
!=
dynamic_cast
<
dve_process_t
*>
(
get_process
(
gb
.
pc
.
gid
))
->
get_commited
(
gb
.
pc
.
lid
))
return
false
;
// may be co enabled if the gid is different (different process)
// or if the lid is the same (same process, same local state)
return
(
ga
.
pc
.
gid
!=
gb
.
pc
.
gid
||
ga
.
pc
.
lid
==
gb
.
pc
.
lid
);
case
GUARD_EXPR
:
// difficult static analysis. Give it a try for simple expressions
break
;
case
GUARD_CHAN
:
return
(
ga
.
chan
.
chan
!=
gb
.
chan
.
chan
||
ga
.
chan
.
sync_mode
==
gb
.
chan
.
sync_mode
);
case
GUARD_COMMITED_FIRST
:
// this only works with local states
if
(
gb
.
type
==
GUARD_PC
)
{
// all non-committed local states may not be co-enabled with this guard
return
(
dynamic_cast
<
dve_process_t
*>
(
get_process
(
gb
.
pc
.
gid
))
->
get_commited
(
gb
.
pc
.
lid
));
}
break
;
}
}
else
{
// if gb is GUARD COMMITED FIRST, reverse the argument order
if
(
gb
.
type
==
GUARD_COMMITED_FIRST
)
return
may_be_coenabled
(
gb
,
ga
);
}
// default
return
true
;
}
void
dve_compiler
::
mark_dependency
(
size_int_t
gid
,
int
type
,
int
idx
,
std
::
vector
<
int
>
&
dep
)
{
...
...
tools/dvecompile.h
View file @
d1b974aa
...
...
@@ -222,6 +222,7 @@ struct dve_compiler: public dve_explicit_system_t
bool
split_conjunctive_expression
(
std
::
vector
<
guard
>&
guard
,
dve_expression_t
*
expr
);
void
merge_dependent_expression
(
std
::
vector
<
guard
>&
guard
,
int
sv_count
);
void
gen_transition_info
();
bool
may_be_coenabled
(
guard
&
ga
,
guard
&
gb
);
void
print_generator
();
};
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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