Skip to content
GitLab
Menu
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
799ab143
Commit
799ab143
authored
Nov 28, 2011
by
Alexandre Duret-Lutz
Browse files
Fix some Doxygen errors.
* src/kripke/kripkeexplicit.hh: Reindent, and fix some comments.
parent
11bb4c77
Changes
2
Hide whitespace changes
Inline
Side-by-side
ChangeLog
View file @
799ab143
2011-11-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix some Doxygen errors.
* src/kripke/kripkeexplicit.hh: Reindent, and fix
some comments.
2011-11-13 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add more nodes when resizing BDD table.
...
...
src/kripke/kripkeexplicit.hh
View file @
799ab143
...
...
@@ -35,60 +35,60 @@ namespace spot
/// \brief Concrete class for kripke states.
class
state_kripke
:
public
state
{
friend
class
kripke_explicit
;
friend
class
kripke_explicit_succ_iterator
;
private:
state_kripke
();
/// \brief Compare two states.
///
/// This method returns an integer less than, equal to, or greater
/// than zero if \a this is found, respectively, to be less than, equal
/// to, or greater than \a other according to some implicit total order.
///
/// For moment, this method only compare the adress on the heap of the
/// twice pointers.
virtual
int
compare
(
const
state
*
other
)
const
;
/// \brief Hash a state
///
/// \FIXME For moment : Only there to can instantiate state_kripke.
virtual
size_t
hash
()
const
;
/// \brief Duplicate a state.
virtual
state_kripke
*
c
l
on
e
()
const
;
/// \brief Add a condition to the conditions already in the state.
/// \param f The condition to add.
void
add_conditions
(
bdd
f
);
/// \brief Add a new successor in the list.
/// \param add_me The state to add.
void
add_succ
(
state_kripke
*
);
virtual
bdd
as_bdd
()
const
{
return
bdd_
;
}
/// \brief Release a state.
///
virtual
void
destroy
()
const
{
}
virtual
~
state_kripke
()
{
}
////////////////////////////////
// Management for succ_iterator
const
std
::
list
<
state_kripke
*>&
get_succ
()
const
;
bdd
bdd_
;
std
::
list
<
state_kripke
*>
succ_
;
friend
class
kripke_explicit
;
friend
class
kripke_explicit_succ_iterator
;
private:
state_kripke
();
/// \brief Compare two states.
///
/// This method returns an integer less than, equal to, or greater
/// than zero if \a this is found, respectively, to be less than, equal
/// to, or greater than \a other according to some implicit total order.
///
/// For moment, this method only compare the adress on the heap of the
/// twice pointers.
virtual
int
compare
(
const
state
*
other
)
const
;
/// \brief Hash a state
virtual
size_t
hash
()
const
;
/// \brief Duplicate a state.
virtual
state_kripke
*
clone
()
const
;
/// \brief Add a condition to the
con
ditions already in the state.
/// \param f The condition to add.
void
add_conditions
(
bdd
f
);
/// \brief Add a new successor in the list.
/// \param succ The successor state to add.
void
add_succ
(
state_kripke
*
succ
);
virtual
bdd
as_bdd
()
const
{
return
bdd_
;
}
/// \brief Release a state.
///
virtual
void
destroy
()
const
{
}
virtual
~
state_kripke
()
{
}
////////////////////////////////
// Management for succ_iterator
const
std
::
list
<
state_kripke
*>&
get_succ
()
const
;
bdd
bdd_
;
std
::
list
<
state_kripke
*>
succ_
;
};
...
...
@@ -96,21 +96,20 @@ namespace spot
/// \brief Implement iterator pattern on successor of a state_kripke.
class
kripke_explicit_succ_iterator
:
public
kripke_succ_iterator
{
public:
kripke_explicit_succ_iterator
(
const
state_kripke
*
,
bdd
);
public:
kripke_explicit_succ_iterator
(
const
state_kripke
*
,
bdd
);
~
kripke_explicit_succ_iterator
();
~
kripke_explicit_succ_iterator
();
virtual
void
first
();
virtual
void
next
();
virtual
bool
done
()
const
;
virtual
void
first
();
virtual
void
next
();
virtual
bool
done
()
const
;
virtual
state_kripke
*
current_state
()
const
;
virtual
state_kripke
*
current_state
()
const
;
private:
const
state_kripke
*
s_
;
std
::
list
<
state_kripke
*>::
const_iterator
it_
;
const
state_kripke
*
s_
;
std
::
list
<
state_kripke
*>::
const_iterator
it_
;
};
...
...
@@ -118,77 +117,74 @@ namespace spot
/// \brief Kripke Structure.
class
kripke_explicit
:
public
kripke
{
public:
kripke_explicit
(
bdd_dict
*
);
kripke_explicit
(
bdd_dict
*
,
state_kripke
*
);
~
kripke_explicit
();
bdd_dict
*
get_dict
()
const
;
state_kripke
*
get_init_state
()
const
;
/// \brief Allow to get an iterator on the state we passed in parameter.
kripke_explicit_succ_iterator
*
succ_iter
(
const
spot
::
state
*
local_state
,
const
spot
::
state
*
global_state
=
0
,
const
tgba
*
global_automaton
=
0
)
const
;
/// \function state_condition
/// \brief Get the condition on the state, designed by the adress,
/// or by his name.
bdd
state_condition
(
const
state
*
s
)
const
;
bdd
state_condition
(
const
std
::
string
)
const
;
/// \brief Return the name of the state.
std
::
string
format_state
(
const
state
*
)
const
;
/// \brief Check if the state already exist, and create it if not.
/// used by the parser for more simplicity.
void
add_state
(
std
::
string
);
/// \function add_transition
/// \brief Add a transition between two state.
/// Allow to do this with the two adress, or just the source adress,
void
add_transition
(
std
::
string
source
,
std
::
string
dest
);
/// \function add_conditions
/// \brief Add a condition in bdd format to the state,
/// name by his name or his address.
/// \param add the condition.
/// \param on_me where add the condition.
void
add_conditions
(
bdd
add
,
std
::
string
on_me
);
/// \brief Add a formula to the state corresponding to the name.
/// \param on_me The state where add.
/// \param f the formula to add.
void
add_condition
(
const
ltl
::
formula
*
f
,
std
::
string
on_me
);
const
std
::
map
<
const
state_kripke
*
,
std
::
string
>&
sn_get
()
const
;
private:
/// \brief Add a state in the two map.
void
add_state
(
std
::
string
,
state_kripke
*
);
void
add_conditions
(
bdd
add
,
state_kripke
*
on_me
);
/// or with the two name.
void
add_transition
(
state_kripke
*
source
,
const
state_kripke
*
dest
);
void
add_transition
(
std
::
string
source
,
const
state_kripke
*
dest
);
bdd_dict
*
dict_
;
state_kripke
*
init_
;
std
::
map
<
const
std
::
string
,
state_kripke
*>
ns_nodes_
;
std
::
map
<
const
state_kripke
*
,
std
::
string
>
sn_nodes_
;
public:
kripke_explicit
(
bdd_dict
*
);
kripke_explicit
(
bdd_dict
*
,
state_kripke
*
);
~
kripke_explicit
();
bdd_dict
*
get_dict
()
const
;
state_kripke
*
get_init_state
()
const
;
/// \brief Allow to get an iterator on the state we passed in
/// parameter.
kripke_explicit_succ_iterator
*
succ_iter
(
const
spot
::
state
*
local_state
,
const
spot
::
state
*
global_state
=
0
,
const
tgba
*
global_automaton
=
0
)
const
;
/// \brief Get the condition on the state
bdd
state_condition
(
const
state
*
s
)
const
;
/// \brief Get the condition on the state
bdd
state_condition
(
const
std
::
string
)
const
;
/// \brief Return the name of the state.
std
::
string
format_state
(
const
state
*
)
const
;
/// \brief Create state, if it does not already exists.
///
/// Used by the parser.
void
add_state
(
std
::
string
);
/// \brief Add a transition between two states.
void
add_transition
(
std
::
string
source
,
std
::
string
dest
);
/// \brief Add a BDD condition to the state
///
/// \param add the condition.
/// \param on_me where add the condition.
void
add_conditions
(
bdd
add
,
std
::
string
on_me
);
/// \brief Add a formula to the state corresponding to the name.
///
/// \param f the formula to add.
/// \param on_me the state where to add.
void
add_condition
(
const
ltl
::
formula
*
f
,
std
::
string
on_me
);
/// \brief Return map between states and their names.
const
std
::
map
<
const
state_kripke
*
,
std
::
string
>&
sn_get
()
const
;
private:
/// \brief Add a state in the two maps.
void
add_state
(
std
::
string
,
state_kripke
*
);
void
add_conditions
(
bdd
add
,
state_kripke
*
on_me
);
void
add_transition
(
std
::
string
source
,
const
state_kripke
*
dest
);
void
add_transition
(
state_kripke
*
source
,
const
state_kripke
*
dest
);
bdd_dict
*
dict_
;
state_kripke
*
init_
;
std
::
map
<
const
std
::
string
,
state_kripke
*>
ns_nodes_
;
std
::
map
<
const
state_kripke
*
,
std
::
string
>
sn_nodes_
;
};
}
#endif
/* !SPOT_KRIPKEEXPLICIT_HH_ */
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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