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
Spot
Spot
Commits
e3a8e9ba
Commit
e3a8e9ba
authored
Apr 22, 2016
by
Etienne Renault
Browse files
intersect: statistic provided using an object
* spot/mc/ec.hh, spot/mc/intersect.hh: here.
parent
5b9c35d0
Changes
2
Hide whitespace changes
Inline
Side-by-side
spot/mc/ec.hh
View file @
e3a8e9ba
...
...
@@ -49,7 +49,7 @@ namespace spot
:
intersect
<
State
,
SuccIterator
,
StateHash
,
StateEqual
,
ec_renault13lpar
<
State
,
SuccIterator
,
StateHash
,
StateEqual
>>
(
sys
,
twa
),
acc_
(
twa
->
acc
())
acc_
(
twa
->
acc
())
,
sccs_
(
0U
)
{
}
...
...
@@ -89,8 +89,10 @@ namespace spot
if
(
top_dfsnum
==
roots_
.
back
().
dfsnum
)
{
roots_
.
pop_back
();
++
sccs_
;
uf_
.
markdead
(
top_dfsnum
);
}
dfs_
=
this
->
todo
.
size
()
>
dfs_
?
this
->
todo
.
size
()
:
dfs_
;
return
true
;
}
...
...
@@ -238,14 +240,10 @@ namespace spot
return
res
;
}
// Refine stats to display
virtual
std
::
string
stats
()
override
virtual
istats
stats
()
override
{
return
std
::
to_string
(
this
->
dfs_number
)
+
" unique states visited
\n
"
+
std
::
to_string
(
roots_
.
size
())
+
" strongly connected components in search stack
\n
"
+
std
::
to_string
(
this
->
transitions
)
+
" transitions explored
\n
"
;
return
{
this
->
states
(),
this
->
trans
(),
sccs_
,
(
unsigned
)
roots_
.
size
(),
dfs_
};
}
private:
...
...
@@ -262,5 +260,7 @@ namespace spot
std
::
vector
<
root_element
>
roots_
;
int_unionfind
uf_
;
acc_cond
acc_
;
unsigned
sccs_
;
unsigned
dfs_
;
};
}
spot/mc/intersect.hh
View file @
e3a8e9ba
...
...
@@ -25,6 +25,17 @@
namespace
spot
{
/// \brief Wrapper to accumulate results from intersection
/// and emptiness checks
struct
SPOT_API
istats
{
unsigned
states
;
unsigned
transitions
;
unsigned
sccs
;
unsigned
instack_sccs
;
unsigned
instack_item
;
};
/// \brief This class explores (with a DFS) a product between a
/// system and a twa. This exploration is performed on-the-fly.
/// Since this exploration aims to be a generic we need to define
...
...
@@ -154,12 +165,9 @@ namespace spot
return
self
().
trace
();
}
virtual
std
::
string
stats
()
virtual
istats
stats
()
{
return
std
::
to_string
(
dfs_number
)
+
" unique states visited
\n
"
+
std
::
to_string
(
transitions
)
+
" transitions explored
\n
"
;
return
{
dfs_number
,
transitions
,
0U
,
0U
,
0U
};
}
protected:
...
...
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