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
56595a15
Commit
56595a15
authored
2 years ago
by
Jaime Arias
Browse files
Options
Downloads
Patches
Plain Diff
refactor code
parent
6653eff7
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/main.cpp
+55
-81
55 additions, 81 deletions
src/main.cpp
with
55 additions
and
81 deletions
src/main.cpp
+
55
−
81
View file @
56595a15
...
...
@@ -132,54 +132,18 @@ net load_net(const string& filename) {
}
/**
* @brief
Compute the set of abstract path from a Petri net model
* @brief
Load observable transitions from a file
* @param model Petri net model
* @param bound SOG bound
* @param obs observable transition
* @param unobs unobservable transitions
* @param g SOG graph
* @param obs_paths observable paths
* @param abstract_paths abstract paths
*/
void
compute_abstract_paths
(
const
net
&
model
,
int
bound
,
const
map
<
int
,
int
>&
obs
,
const
set
<
int
>&
unobs
,
MDGraph
&
g
,
paths_t
&
obs_paths
,
paths_t
&
abstract_paths
)
{
// build the SOG
cout
<<
"Building SOG ..."
;
RdPBDD
SOG
(
model
,
obs
,
unobs
,
bound
);
cout
<<
" done"
<<
endl
;
// compute the observable paths
obs_paths
=
SOG
.
chem_obs
(
g
,
obs
);
// add abstract paths
for
(
auto
path
:
obs_paths
)
{
abstract_paths
.
insert
(
SOG
.
chem_abs
(
path
,
g
));
}
}
/**
* @brief Generates abstract paths of a Petri net covering transitions specified
* in a file
* @param net_file Path to file of the petri net model
* @param bound SOG bound
* @param transitions_file Path to file of observable transitions
* @param output_folder Path to folder where output files will be saved
* @param file Path to the file with the observable transitions
* @param obs_trans set of observable transitions
* @param unobs_trans set of unobservable transitions
*/
void
generate_paths_from_file
(
const
string
&
net_file
,
int
bound
,
const
string
&
transitions_file
,
const
string
&
output_folder
)
{
net
model
=
load_net
(
net_file
);
string
model_name
=
get_model_name
(
net_file
);
// TODO: should we take into account reading the file ?
double
d
=
getTime
();
// get observable transitions from file
void
load_transitions
(
const
net
&
model
,
const
string
&
file
,
map
<
int
,
int
>&
obs_trans
,
set
<
int
>&
unobs_trans
)
{
string
line
;
ifstream
my_file
(
transitions_file
);
map
<
int
,
int
>
obs_trans
;
// TODO: <transition_id, _>
ifstream
my_file
(
file
);
// TODO: What means the second element of obs_trans type ? {<tr_id>, 1}
if
(
my_file
)
{
while
(
getline
(
my_file
,
line
))
{
// TODO: catch error when the file has transition different to t
...
...
@@ -190,65 +154,79 @@ void generate_paths_from_file(const string& net_file, int bound,
// TODO: What happens if the transition started in t1 instead of t0 ?
// compute the unobservable transitions
set
<
int
>
unobs_trans
;
for
(
long
unsigned
int
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
obs_trans
.
find
(
i
))
==
obs_trans
.
end
())
{
unobs_trans
.
insert
(
i
);
}
}
}
// compute abstract paths
MDGraph
g
;
paths_t
obs_paths
;
paths_t
abstract_paths
;
compute_abstract_paths
(
model
,
bound
,
obs_trans
,
unobs_trans
,
g
,
obs_paths
,
abstract_paths
);
// time for generating the paths
float
tps
=
getTime
()
-
d
;
/**
* @brief 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
*/
void
find_observable_transitions
(
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
();
// print output
string
output_file
=
output_folder
+
"/no_optimal_"
+
model_name
+
".txt"
;
print_output
(
model
,
g
,
obs_trans
,
obs_paths
,
abstract_paths
,
tps
,
output_file
);
// compute the observable transitions
for
(
long
unsigned
int
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
unobs_trans
.
find
(
i
))
==
unobs_trans
.
end
())
{
obs_trans
.
insert
({
i
,
1
});
}
}
}
/**
* @brief Generate abstract paths of a Petri net covering all the observable
* transitions
* @brief Generate abstract paths of a Petri net
* @param net_file Path to file of the petri net model
* @param bound SOG bound
* @param transitions_file Path to file of observable transitions
* @param output_folder Path to folder where output files will be saved
*/
void
generate_all_paths
(
const
string
&
net_file
,
int
bound
,
const
string
&
output_folder
)
{
void
compute_abstract_paths
(
const
string
&
net_file
,
int
bound
,
const
string
&
transitions_file
,
const
string
&
output_folder
)
{
net
model
=
load_net
(
net_file
);
string
model_name
=
get_model_name
(
net_file
);
double
d
=
getTime
();
// compute the unobservable transitions of the model using the pattern
set
<
int
>
unobs_trans
=
model
.
calcul1
();
// compute the observable transitions
// find observable transitions
set
<
int
>
unobs_trans
;
map
<
int
,
int
>
obs_trans
;
for
(
long
unsigned
int
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
unobs_trans
.
find
(
i
))
==
unobs_trans
.
end
())
{
obs_trans
.
insert
({
i
,
1
});
}
// if a path with transitions is not given, then we apply the algorithm to
// find the needed observable transitions to cover all the behaviors
if
(
transitions_file
==
""
)
{
find_observable_transitions
(
model
,
obs_trans
,
unobs_trans
);
}
else
{
load_transitions
(
model
,
transitions_file
,
obs_trans
,
unobs_trans
);
}
// compute abstract paths
// build the SOG
cout
<<
"Building SOG ..."
;
MDGraph
g
;
paths_t
obs_paths
;
RdPBDD
SOG
(
model
,
obs_trans
,
unobs_trans
,
bound
);
cout
<<
" done"
<<
endl
;
// compute the observable paths
paths_t
obs_paths
=
SOG
.
chem_obs
(
g
,
obs_trans
);
// add abstract paths
paths_t
abstract_paths
;
compute_abstract_paths
(
model
,
bound
,
obs_trans
,
unobs_trans
,
g
,
obs_paths
,
abstract_paths
);
for
(
auto
path
:
obs_paths
)
{
abstract_paths
.
insert
(
SOG
.
chem_abs
(
path
,
g
));
}
// time for generating the paths
float
tps
=
getTime
()
-
d
;
// print output
string
model_name
=
get_model_name
(
net_file
);
string
output_file
=
output_folder
+
"/no_optimal_"
+
model_name
+
".txt"
;
print_output
(
model
,
g
,
obs_trans
,
obs_paths
,
abstract_paths
,
tps
,
output_file
);
...
...
@@ -285,11 +263,7 @@ int main(int argc, char** argv) {
CLI11_PARSE
(
app
,
argc
,
argv
);
int
bound
=
32
;
if
(
*
opt_transitions
)
{
generate_paths_from_file
(
input_file
,
bound
,
obs_file
,
output_folder
);
}
else
{
generate_all_paths
(
input_file
,
bound
,
output_folder
);
}
compute_abstract_paths
(
input_file
,
bound
,
obs_file
,
output_folder
);
return
0
;
}
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