Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
sogMBT
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
PMC-SOG
sogMBT
Commits
b62902d3
Commit
b62902d3
authored
4 months ago
by
Jaime Arias
Browse files
Options
Downloads
Patches
Plain Diff
refactor: remove TODOs
parent
66ce5a29
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
src/main.cpp
+26
-15
26 additions, 15 deletions
src/main.cpp
src/petri_net_sog.cpp
+6
-8
6 additions, 8 deletions
src/petri_net_sog.cpp
with
32 additions
and
23 deletions
src/main.cpp
+
26
−
15
View file @
b62902d3
#include
<CLI11.hpp>
#include
<ctime>
#include
<fstream>
#include
<iomanip>
#include
<iostream>
#include
<map>
#include
<regex>
#include
<string>
#include
"Net.hpp"
...
...
@@ -11,7 +11,6 @@
#include
"petri_net_sog.hpp"
// BDD initial values
// TODO: these values are also defined in petri_net_sog.cpp
constexpr
int
BDD_INITIAL_NUM_NODES
=
10000
;
constexpr
int
BDD_SIZE_CACHES
=
10000
;
...
...
@@ -23,6 +22,16 @@ double GetTime() {
return
static_cast
<
double
>
(
clock
())
/
static_cast
<
double
>
(
CLOCKS_PER_SEC
);
}
/**
* Check if a string is a valid transition name
* @param str transition name
* @return true if the transition name is valid, false otherwise
*/
bool
ValidTransitionName
(
const
std
::
string
&
str
)
{
const
std
::
regex
pattern
(
"^t
\\
d+$"
);
return
std
::
regex_match
(
str
,
pattern
);
}
/**
* Save in a file the information about observable paths
* @param output_file Path to the file where the output will be saved
...
...
@@ -133,42 +142,44 @@ void LoadTransitions(const net& model, const string& file,
map
<
int
,
int
>&
obs_trans
,
set
<
int
>&
unobs_trans
)
{
ifstream
my_file
(
file
);
// TODO: What means the second element of obs_trans type ? {<tr_id>, 1}
if
(
my_file
)
{
string
line
;
while
(
getline
(
my_file
,
line
))
{
// TODO: catch error when the file has transition different to t
// check if the transition name is valid
if
(
!
ValidTransitionName
(
line
))
{
cerr
<<
"Error: Invalid transition name: "
<<
line
<<
'\n'
;
exit
(
1
);
}
// for a transition t1, we take the 1 as the number of occurrences
int
trans_id
=
stoi
(
line
.
substr
(
1
));
obs_trans
.
insert
({
trans_id
,
1
});
}
}
// TODO: What happens if the transition started in t1 instead of t0 ?
// compute the unobservable transitions
for
(
auto
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
obs_trans
.
find
(
i
))
==
obs_trans
.
end
())
{
unobs_trans
.
insert
(
i
);
for
(
auto
t
=
0
;
t
<
model
.
transitions
.
size
();
t
++
)
{
if
((
obs_trans
.
find
(
t
))
==
obs_trans
.
end
())
{
unobs_trans
.
insert
(
t
);
}
}
}
/**
* Find the observable transitions needed for covering all the model
* @param model Petri net model
* @param obs_trans set of observable transitions
* @param unobs_trans set of unobservable transitions
* @param
[in]
model Petri net model
* @param
[out]
obs_trans set of observable transitions
* @param
[out]
unobs_trans set of unobservable transitions
*/
void
FindObservableTransitions
(
net
&
model
,
map
<
int
,
int
>&
obs_trans
,
set
<
int
>&
unobs_trans
)
{
// compute the unobservable transitions of the model using the pattern
// TODO: why cannot be const model ?
unobs_trans
=
model
.
calcul1
();
// compute the observable transitions
for
(
auto
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
unobs_trans
.
find
(
i
))
==
unobs_trans
.
end
())
{
obs_trans
.
insert
({
i
,
1
});
for
(
auto
t
=
0
;
t
<
model
.
transitions
.
size
();
t
++
)
{
if
((
unobs_trans
.
find
(
t
))
==
unobs_trans
.
end
())
{
obs_trans
.
insert
({
t
,
1
});
}
}
}
...
...
This diff is collapsed.
Click to expand it.
src/petri_net_sog.cpp
+
6
−
8
View file @
b62902d3
...
...
@@ -57,10 +57,10 @@ int SelectFirableTrans(Set covered_trans, const Set &firable_trans) {
return
-
1
;
}
void
ReinitCycle
(
const
vector
<
int
>
&
sw
,
map
<
int
,
int
>
&
trans_obs
)
{
for
(
auto
i
:
sw
)
{
if
(
trans_obs
[
i
]
>
0
)
{
trans_obs
[
i
]
=
2
;
void
ReinitCycle
(
const
Path
&
trace
,
map
<
int
,
int
>
&
trans_obs
)
{
for
(
auto
t
:
trace
)
{
if
(
trans_obs
[
t
]
>
0
)
{
trans_obs
[
t
]
=
2
;
}
}
}
...
...
@@ -301,12 +301,10 @@ Paths PetriNetSOG::ObservablePaths(SOG &sog, map<int, int> trans_obs) const {
// construction of the first aggregate
auto
*
c
=
new
Aggregate
;
{
bdd
complete_aggr
=
AccessibleEpsilon
(
m0
);
const
bdd
complete_aggr
=
AccessibleEpsilon
(
m0
);
c
->
state
=
complete_aggr
;
firable_trans
=
FirableObservableTrans
(
complete_aggr
);
// TODO: why create a couple if c already contains the state aggregate?
st
.
emplace
(
c
,
firable_trans
);
}
...
...
@@ -349,7 +347,7 @@ Paths PetriNetSOG::ObservablePaths(SOG &sog, map<int, int> trans_obs) const {
elt
.
firable_trans
.
erase
(
t
);
st
.
push
(
elt
);
//
double nbnode;
//
computes the successor
{
auto
*
reached_aggr
=
new
Aggregate
;
bdd
complete_aggr
=
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
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!
Save comment
Cancel
Please
register
or
sign in
to comment