Implementation of a Coupled Similarity Checker #1619
Conversation
|
Thanks for this contribution! My response is somewhat delayed due to the holidays. On first glance, your code looks good. I think the data structures can be improved if you want to be able to handle larger transition systems. I will have a detailed look at it some time this week. |
|
Thanks for your response. I am looking forward to it. For my own usecases I had some |
There was a problem hiding this comment.
I have added some inline comments that may help you improve some details of the implementation. As for the data structures, I currently don't have a deep enough understanding of the algorithm to give a clear idea about what is optimal. I do have a hint that might guide you in the right direction: have a look at the data structures used for storing parity games in one of our libraries. Here, the nodes are stored in a vector and indexed by their position in the vector. This allows for much faster lookup than in a large map.
| stream << (l1.action_label(a)); | ||
| move_label = stream.str(); | ||
| stream.str(""); | ||
| stream.clear(); |
There was a problem hiding this comment.
Perhaps this can be simplified with the std::to_string function.
| { | ||
| if (node_winner.find(n) == node_winner.end()) | ||
| { | ||
| std::cerr |
There was a problem hiding this comment.
It would be nice to consistently use mCRL2log. That output also goes to stderr, by the way. You can always use a higher log level such as log::warning or log::error to ensure this output is shown.
| } | ||
| else // just extend simply. | ||
| { | ||
| for (const auto &ntrans : next) |
There was a problem hiding this comment.
We allow C++17 code, so you can use a structured binding here to make the code even more compact.
This new equivalence checks the two root processes for coupled simulation equivalence, introduced by Parrow and Sjödin in 1992 [PS92]. The algorithm uses the game theoretic approach of Bisping and Nestmann from 2019 [BN19]. The algorithm will return equality, if the root processes are coupled similar. Additionally it calculates the set R, which can be shown with the `ltscompare` flag `--debug`.
Noxsense
force-pushed
the
feat-coupled_sim_equiv
branch
from
2ae5a5f
to
87b26dd
Compare
|
|
||
| std::map<cs_game_move, bool> todo_if; | ||
|
|
||
| // TODO this includes also weak, as challenge giver invalid, solve! |
There was a problem hiding this comment.
Does this TODO item mean that the implemented algorithm is not yet fully correct? If so, what steps are necessary in order to finalise the algorithm. Same remark on line 419.
| cs_game_node from, to; | ||
| size_t act; | ||
| std::string label_of_action; | ||
| bool weak; |
There was a problem hiding this comment.
This 'weak' field is only read from and never assigned to.
| if (len < 1) // no further steps. | ||
| { | ||
| continue; | ||
| } | ||
| else // just extend simply. |
There was a problem hiding this comment.
This is the same as if (len >= 1). Also on line 295.
|
This pull request has been open for some time and it is a worthwhile addition for our tool set. Therefore, I have resolved the relatively minor comments locally and have also added the small example from the 2019 paper as a test case. EDIT: I can actually push my commits to your branch. |
| if (true) // also just tau chains may be later used | ||
| // if (already_good) // (actually already) done | ||
| { |
There was a problem hiding this comment.
Here, the comments indicate an alternative condition, but it is not clear what should be chosen. Same on line 285.
There was a problem hiding this comment.
With this whole block, starting at L200, I wanted to create weak transitions, since I wasn't sure there was a already method supporting such things. So I created my own weak_transitions struct there and fetched all weak transitions.
The actual if (true) block had an old condition, I didn't use anymore and was later abused as indentation.
|
Yeah, I am sorry, I have not fixed those issues yet, since I was busy and later My old TODOs are working and correct in a very naive way. But I added those (And maintainers are allowed to edit for this commit.) |
|
No problem. If the TODO's are only further performance improvements then I propose that we merge this pull request as it is now so that other users can also experiment with coupled similarity. Whenever the new algorithm is finished you can then open a new pull request to update the implementation. |
mlaveaux
changed the title
For my bachelor thesis I extended
ltscomparewith an algorithm which checks for Coupled Similarity[PS92]. Now I want to make it a merge-able and maintainable part of your code base.By now it just compares the input and returns a boolean saying wether they are equal by definition with a suggested algorithm that uses a game theoretic approach [BN19].
Due to only limited insight to all possibilities this whole project offers, I might have not made very effective decisions and I am very thankful for any suggestions and tips for what I could improve, please.
I may also want to extend my contribution to
ltsconvertat a later time.Various tests will follow soonish.
[PS92] Parrow, Joachim and Sjödin, Peter: Multiway synchronization verified with coupled simulation. Springer Berlin Heidelberg, 1992.
[BN19] Bisping, Benjamin and Nestmann, Uwe: Computing Coupled Similarity. Springer International Publishing, 2019.