forked from ticktac-project/tchecker
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Alexander Lieb
committed
Dec 12, 2024
1 parent
f0450f3
commit 22c3b5d
Showing
26 changed files
with
279 additions
and
292 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
72 changes: 72 additions & 0 deletions
72
include/tchecker/strong-timed-bisim/contradiction_searcher.hh
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,72 @@ | ||
| /* | ||
| * This file is a part of the TChecker project. | ||
| * | ||
| * See files AUTHORS and LICENSE for copyright details. | ||
| * | ||
| */ | ||
|
|
||
| #ifndef TCHECKER_STRONG_TIMED_BISIM_SEARCH_CONTRADICTION_HH | ||
| #define TCHECKER_STRONG_TIMED_BISIM_SEARCH_CONTRADICTION_HH | ||
|
|
||
| #include "tchecker/vcg/virtual_constraint.hh" | ||
|
|
||
| namespace tchecker { | ||
|
|
||
| namespace strong_timed_bisim { | ||
|
|
||
| class contradiction_searcher_t { | ||
|
|
||
| public: | ||
|
|
||
| /*! | ||
| \brief Constructor | ||
| */ | ||
| contradiction_searcher_t(std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B, | ||
| tchecker::clock_id_t no_of_virt_clks); | ||
|
|
||
| /*! | ||
| \brief finds a contradiction to timed bisimulation | ||
| \param zone_A : the zone of the first symbolic state | ||
| \param zone_B : the zone of the second symbolic state | ||
| \param trans_A : the outgoing transitions of the first symbolic state | ||
| \param trans_B : the outgoing transitions of the second symbolic state | ||
| \param found_cont : the matrix where the already found contradictions of the outgoing transitions are stored | ||
| */ | ||
| std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> | ||
| search_contradiction(tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B, | ||
| std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B, | ||
| tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_t> found_cont); | ||
|
|
||
| /*! | ||
| \brief checks whether it makes sense to go on searching for contradictions | ||
| \param zone_A : the zone of the first symbolic state | ||
| \param zone_B : the zone of the second symbolic state | ||
| \param trans_A : the outgoing transitions of the first symbolic state | ||
| \param trans_B : the outgoing transitions of the second symbolic state | ||
| \param found_cont : the matrix where the already found contradictions of the outgoing transitions are stored | ||
| \param finished : the matrix which says at which pairs all contradictions are already found | ||
| */ | ||
| bool | ||
| contradiction_still_possible(tchecker::zg::zone_t const & zone_A, tchecker::zg::zone_t const & zone_B, | ||
| std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_A, | ||
| std::vector<tchecker::vcg::vcg_t::sst_t *> & trans_B, | ||
| tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_t> & found_cont, | ||
| std::vector< std::vector<bool> > finished); | ||
| private: | ||
|
|
||
| tchecker::zone_matrix_t<tchecker::virtual_constraint::virtual_constraint_t> overhangs; | ||
| tchecker::clock_id_t no_of_virt_clks; | ||
|
|
||
| contradiction_searcher_t(); | ||
|
|
||
| std::shared_ptr<tchecker::zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>> | ||
| find_contradiction(tchecker::zg::zone_t const & zone, std::vector<tchecker::vcg::vcg_t::sst_t *> & trans, | ||
| std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> & found_con, | ||
| std::vector<std::shared_ptr<zone_container_t<tchecker::virtual_constraint::virtual_constraint_t>>> & cur_overhang); | ||
|
|
||
| }; | ||
|
|
||
| } // end of namespace strong_timed_bisim | ||
|
|
||
| } // end of namespace tchecker | ||
| #endif |
34 changes: 0 additions & 34 deletions
34
include/tchecker/strong-timed-bisim/search_contradiction.hh
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.