Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
divine-ltsmin-deb
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Spot
divine-ltsmin-deb
Commits
968e52ff
Commit
968e52ff
authored
Apr 23, 2013
by
Alfons Laarman
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
NDA incomplete
parent
5addfe60
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
42 additions
and
0 deletions
+42
-0
tools/dvecompile.cpp
tools/dvecompile.cpp
+41
-0
tools/dvecompile.h
tools/dvecompile.h
+1
-0
No files found.
tools/dvecompile.cpp
View file @
968e52ff
...
...
@@ -2391,6 +2391,40 @@ void dve_compiler::gen_transition_info()
block_end
();
line
();
////////////////////////////////////////////////
// EXPORT DO NOT ACCORD MATRIX //
////////////////////////////////////////////////
// guard nes matrix (#guards x #transitions)
snprintf
(
buf
,
BUFLEN
,
"int nda[%zu][%zu] = "
,
transitions
.
size
(),
transitions
.
size
());
line
(
buf
);
block_begin
();
for
(
size_int_t
i
=
0
;
i
<
transitions
.
size
();
i
++
)
{
append
(
"{"
);
for
(
size_int_t
j
=
0
;
j
<
transitions
.
size
();
j
++
)
{
if
(
j
!=
0
)
append
(
", "
);
append
(
is_nda
(
transitions
[
i
],
transitions
[
j
])
?
"1"
:
"0"
);
}
if
(
i
==
guard
.
size
()
-
1
)
line
(
"}"
);
else
line
(
"},"
);
}
block_end
();
line
(
";"
);
line
();
// guard nes function
line
(
"extern
\"
C
\"
const int* get_nda_matrix(int t) "
);
block_begin
();
snprintf
(
buf
,
BUFLEN
,
"if (t >= 0 && t < %zu) return nda[t];"
,
transitions
.
size
());
line
(
buf
);
snprintf
(
buf
,
BUFLEN
,
"return NULL;"
);
line
(
buf
);
block_end
();
line
();
////////////////////////////////////////////////
// EXPORT NECESSARY DISABLING SETS FOR GUARDS //
////////////////////////////////////////////////
...
...
@@ -2476,6 +2510,13 @@ bool dve_compiler::is_guard_nds( guard& g, ext_transition_t& t ) {
return
true
;
}
bool
dve_compiler
::
is_nda
(
ext_transition_t
&
t1
,
ext_transition_t
&
t2
)
{
if
(
t1
.)
{
}
return
true
;
}
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
)
{
...
...
tools/dvecompile.h
View file @
968e52ff
...
...
@@ -236,6 +236,7 @@ struct dve_compiler: public dve_explicit_system_t
bool
get_const_expression
(
dve_expression_t
&
expr
,
int
&
value
);
bool
is_guard_nes
(
guard
&
g
,
ext_transition_t
&
t
);
bool
is_guard_nds
(
guard
&
g
,
ext_transition_t
&
t
);
bool
dve_compiler
::
is_nda
(
ext_transition_t
&
t1
,
ext_transition_t
&
t2
);
bool
may_be_coenabled
(
guard
&
ga
,
guard
&
gb
);
void
extract_predicates
(
std
::
vector
<
simple_predicate
>&
p
,
dve_expression_t
&
e
);
bool
is_conflict_predicate
(
simple_predicate
&
p1
,
simple_predicate
p2
);
...
...
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