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
5fce878b
Commit
5fce878b
authored
2 years ago
by
Jaime Arias
Browse files
Options
Downloads
Patches
Plain Diff
fix print
parent
c9726523
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
+35
-8
35 additions, 8 deletions
src/main.cpp
with
35 additions
and
8 deletions
src/main.cpp
+
35
−
8
View file @
5fce878b
...
...
@@ -25,7 +25,7 @@ void save_observable_paths(const string& model_name,
cout
<<
"Saving results in "
<<
output_file
<<
endl
;
ofstream
monFlux
(
output_file
);
monFlux
<<
"#
observable
paths: "
<<
obs_paths
.
size
()
<<
endl
;
monFlux
<<
"# paths: "
<<
obs_paths
.
size
()
<<
endl
;
int
n
=
1
;
for
(
auto
path
:
obs_paths
)
{
...
...
@@ -116,9 +116,17 @@ void compute_abstract_paths(const net& model, MDGraph& g,
}
}
void
get_transitions_from_file
(
const
net
&
model
,
const
string
&
file
,
map
<
int
,
int
>&
obs
,
set
<
int
>&
unobs
)
{
ifstream
flux
(
file
);
void
generate_paths_from_file
(
const
string
&
net_file
,
const
string
&
transitions_file
,
const
string
&
output_folder
,
int
bound
=
32
)
{
net
model
=
load_net
(
net_file
);
string
model_name
=
get_model_name
(
net_file
);
double
d
=
getTime
();
// get observable transitions from file
map
<
int
,
int
>
obs
;
ifstream
flux
(
transitions_file
);
string
ligne
;
if
(
flux
)
{
while
(
getline
(
flux
,
ligne
))
{
...
...
@@ -126,11 +134,28 @@ void get_transitions_from_file(const net& model, const string& file,
obs
.
insert
({
tr
,
1
});
}
}
// compute the unobservable transitions
set
<
int
>
unobs
;
for
(
long
unsigned
int
i
=
0
;
i
<
model
.
transitions
.
size
();
i
++
)
{
if
((
obs
.
find
(
i
))
==
obs
.
end
())
{
unobs
.
insert
(
i
);
}
}
// compute abstract paths
MDGraph
g
;
set
<
vector
<
int
>>
obs_paths
;
set
<
vector
<
int
>>
abstract_paths
;
compute_abstract_paths
(
model
,
g
,
obs
,
unobs
,
obs_paths
,
abstract_paths
,
bound
);
// time for generating the paths
double
tps
=
getTime
()
-
d
;
// print output
print_output
(
model
,
g
,
obs
,
obs_paths
,
abstract_paths
,
tps
,
model_name
,
output_folder
);
}
void
generate_all_paths
(
const
string
&
net_file
,
const
string
&
output_folder
,
...
...
@@ -203,7 +228,7 @@ int main(int argc, char** argv) {
->
fallthrough
();
std
::
string
obs_file
;
generate
->
add_option
(
"--
transitions
"
,
obs_file
,
"Observable transitions"
)
generate
->
add_option
(
"--
obs-file
"
,
obs_file
,
"Observable transitions"
)
->
type_name
(
"Path"
)
->
check
(
CLI
::
ExistingFile
);
...
...
@@ -214,9 +239,11 @@ int main(int argc, char** argv) {
// reach->callback([&]() {});
// sog->callback([&]() {});
generate
->
callback
([
&
]()
{
// if (all) {
generate_all_paths
(
input_file
,
output_folder
);
// }
if
(
all
)
{
generate_all_paths
(
input_file
,
output_folder
);
}
else
{
generate_paths_from_file
(
input_file
,
obs_file
,
output_folder
);
}
});
// parse arguments
...
...
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