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
VIGNET Pierre
cadbiom
Commits
1507bf34
Commit
1507bf34
authored
Jan 28, 2020
by
VIGNET Pierre
Browse files
[lib] get_frontier_scc() small refactor on ugly code...
parent
7823a878
Changes
1
Hide whitespace changes
Inline
Side-by-side
library/cadbiom/models/guard_transitions/analyser/static_analysis.py
View file @
1507bf34
...
...
@@ -339,66 +339,67 @@ class StaticAnalyzer(object):
frontier_list
=
[]
tvi
=
TableVisitor
(
self
.
reporter
)
self
.
model
.
accept
(
tvi
)
print
(
"Table visitor"
,
tvi
)
for
scc
in
scc_list
:
# eliminate isolated frontier nodes
if
len
(
scc
)
>
1
:
frontier
=
True
# generate symbol table for partial evaluation
# all places in scc are inactivated (-1)
symbol_table
=
dict
.
fromkeys
(
scc
,
-
1
)
pe_visitor
=
EstimExpVisitor
(
symbol_table
)
# find all incoming transitions for each node in scc
LOGGER
.
debug
(
"scc: "
+
str
(
scc
))
for
node_name
in
scc
:
try
:
# raises keyerror if the model isn't reloaded manually..
chart_node
=
self
.
model
.
node_dict
[
node_name
]
except
KeyError
:
return
list
([[
"Error: Please try by
\
saving & reloading the model manually"
]])
for
in_trans
in
chart_node
.
incoming_trans
:
LOGGER
.
debug
(
"Node {}, trans: {}"
.
format
(
node_name
,
(
in_trans
.
ori
.
name
,
in_trans
.
ext
.
name
)
)
)
if
len
(
scc
)
<=
1
:
continue
frontier
=
True
# generate symbol table for partial evaluation
# all places in scc are inactivated (-1)
symbol_table
=
dict
.
fromkeys
(
scc
,
-
1
)
pe_visitor
=
EstimExpVisitor
(
symbol_table
)
# if the transition comes from outside scc,
# we try to detect if scc may be reached with this trans
# Note: this time we use the real symb_table with
# frontiers active; not a fake one with all places in scc
# disabled.
# TODO: detect if the in_transition comes from a frontier
# may be sufficient to detect if the SCC is reachable.
if
in_trans
.
ori
.
name
not
in
scc
:
cond
=
self
.
__tr_estim
(
in_trans
,
pe_visitor
,
tvi
.
tab_symb
)
# a mon avis, ne renvoie jamais un resultat superieur a 0
# car tvi.tab_symb initialise toutes les places a 0
# et pe_visitor est initialise avec les places de la SCC a -1
# le 1 (True) semble impossible (sauf oposition de signe
# avec l'operateur not).
# LOGGER.warning(
# "scc validated as a cyle ?: " + str(cond)
# )
# Guard of the transition is True
# (not False or indeterminate),
# so scc may be reached from other part of the model
# => switch to next scc
if
cond
>=
0
:
frontier
=
False
break
if
frontier
:
LOGGER
.
debug
(
"frontier found"
)
frontier_list
.
append
(
scc
)
# find all incoming transitions for each node in scc
LOGGER
.
debug
(
"scc: "
+
str
(
scc
))
for
node_name
in
scc
:
try
:
# raises keyerror if the model isn't reloaded manually..
chart_node
=
self
.
model
.
node_dict
[
node_name
]
except
KeyError
:
return
list
([[
"Error: Please try by
\
saving & reloading the model manually"
]])
for
in_trans
in
chart_node
.
incoming_trans
:
LOGGER
.
debug
(
"Node {}, trans: {}"
.
format
(
node_name
,
(
in_trans
.
ori
.
name
,
in_trans
.
ext
.
name
)
)
)
# if the transition comes from outside scc,
# we try to detect if scc may be reached with this trans
# Note: this time we use the real symb_table with
# frontiers active; not a fake one with all places in scc
# disabled.
# TODO: detect if the in_transition comes from a frontier
# may be sufficient to detect if the SCC is reachable.
if
in_trans
.
ori
.
name
not
in
scc
:
cond
=
self
.
__tr_estim
(
in_trans
,
pe_visitor
,
tvi
.
tab_symb
)
# a mon avis, ne renvoie jamais un resultat superieur a 0
# car tvi.tab_symb initialise toutes les places a 0
# et pe_visitor est initialise avec les places de la SCC a -1
# le 1 (True) semble impossible (sauf oposition de signe
# avec l'operateur not).
# LOGGER.warning(
# "scc validated as a cyle ?: " + str(cond)
# )
# Guard of the transition is True
# (not False or indeterminate),
# so scc may be reached from other part of the model
# => switch to next scc
if
cond
>=
0
:
frontier
=
False
break
if
frontier
:
LOGGER
.
debug
(
"frontier found"
)
frontier_list
.
append
(
scc
)
LOGGER
.
debug
(
"SCC found: "
+
str
(
frontier_list
))
...
...
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