Parse of atomic propositions in LTSmin wrapper
Currently syntax for atomic propositions in LTSmin/PINS wrapper is pretty limited : it comes down to "var X op constant value" with op in ==,!=,>,<,>=...
This patch introduces an actual AST for these atomic propositions, so that we also get :
- var1 op var2
- cte op var ... and prepares for extension to e.g. sum of variables on one side.
I've used shared_ptr to store children of a node, but maybe unique_ptr would actually be more appropriate since there is currently no aliasing of subexpressions.
I cannot create a "Merge request" (more permission issues it seems), so I put the code in a GitHub hosted fork, since I can't fork here either.
So, I want to merge : https://github.com/yanntm/spot/tree/ytm/parse (i.e. branch ytm/parse of my fork) back into your code base (probably into "next").
I only edited file ltsmin.cc, and branched off of next.
I'm pretty sure my code does not satisfy every spot committer constraint, e.g. I was unable to reindent the file correctly without busting the original indentation, I did not really make sure there are no > 80 char lines (do you still enforce that ?) etc... Ill be happy to edit it until it conforms to the guidelines as soon as I get a CI run on your server that checks these things.
I also had to fight with the compiler to get it to accept my : shared_ptr instances+assignment, probably I did not do it the right way (I end up with a lot of "new" in the code, which I though I could avoid). Meh, I'm still not very fluent in modern C++ it seems (doing too much Java, and Java is too easy :D).
If I could get an upgraded account that would be helpful, to keep things on this gitlab instance etc... I might have more code to submit in the near future as we are working on this MCC/spot submission with @renault.