Issue 31: Added SPOT 2.X wrapper #82

cjbanks · 2022-01-17T21:28:10Z

Hi, I've managed to create the wrapper for SPOT 2.X in order to enhance compatibility with Texada. Could you take a look and let me know if you have any questions/comments? I also ran ./texadatest with the following output:

[----------] Global test environment tear-down
[==========] 63 tests from 13 test suites ran. (6218 ms total)
[ PASSED ] 61 tests.
[ FAILED ] 2 tests, listed below:
[ FAILED ] AtomicPropositionSubbingClonerTest.SimpleTest
[ FAILED ] AtomicPropositionSubbingClonerTest.SimpleConstantEventTest

2 FAILED TESTS
YOU HAVE 2 DISABLED TESTS

If you have any suggestions on how to pass these last two tests that would be very helpful. Thanks!

…om SPOT

…mula calls

… the wrapper

Mapping files have updated the previous class/function calls to reside in texada namespace instead of spot since these calls may be defunct in SPOT 2.X

Cannot use SPOT namespace with current object calls so we use the texada namespace and use the mappings created for Texada

carolemieux · 2022-01-19T18:31:36Z

Wow, thank you so much for the contribution! Let me have a look at the changes and in particular the failing tests --- I should be able to get to this sometime next week.

carolemieux · 2022-01-27T18:07:28Z

texada-src/src/checkers/prefixtreechecker.cpp

@@ -980,6 +980,8 @@ map<int, statistic> prefix_tree_checker::not_map(map<int, statistic> map) {
 */
 void prefix_tree_checker::add_satisfying_values(map<int, statistic>& returned_vals,
        bool to_satisfy, map<int, statistic>& map_to_return, set<int>& to_check) {
+


Can remove this extra whitespace.

carolemieux · 2022-01-27T18:13:10Z

texada-src/src/main/texadamain.cpp

@@ -336,9 +338,9 @@ int main(int ac, char* av[]) {
                        outFile << ", ";
                    print_json(outFile, *it, opts_map.count("print-stats"));
                } else {
-                    const spot::ltl::formula * valid_form = texada::instantiate(
+                    const ltl::formula * valid_form = texada::instantiate(


If we're using namespace texada, why do we need texada::instantiate rather than just instantiate?

This is true, we can use just instantiate.

carolemieux · 2022-01-27T18:15:07Z

texada-src/tests/constinstantspool_test.cpp

@@ -68,15 +67,15 @@ TEST(ConstInstantsPoolTest,UsableByLinearChecker) {
    ASSERT_EQ(l_valid_instants.at(0).first.at("a"), "a");
    ASSERT_EQ(l_valid_instants.at(0).first.at("c"), "c");

-    f->destroy();
+    //f->destroy();


why is f->destroy removed in this test?

SPOT 2.X does not use the destroy function externally like this anymore, a lot of the destruction of formula classes is done internally. In this test, the instantiated_prop_type used in 'valid_instants_on_traces' instantiated the formula by recusing on the formula. In this case, when creating the visitor this is just returning the pointer to the formula so when destroy is called in the function it is also destroying the original formula.

carolemieux · 2022-01-27T18:17:38Z

texada-src/tests/propertytypeminer_test.cpp

@@ -9,8 +9,7 @@
 #include "../src/main/opts.h"
 #include "../src/checkers/statistic.h"
 #include <gtest/gtest.h>
-#include <ltlvisit/tostring.hh>
-#include <ltlparse/public.hh>
+#include "../src/instantiation-tools/texadatospotmapping.h"


is this import necessary? It doesn't look like this is used anywhere.

carolemieux · 2022-01-27T18:21:01Z

(left a few minor comments above, hoping to tackle the core of the review tomorrow)

carolemieux · 2022-02-01T15:45:44Z

Thanks again for the contribution :). I looked at the overall changes. The PR works great overall, I got everything running against the latest version of SPOT! Two main things remain:

The failing test case is due to the use of the str_spin_ltl function (https://spot.lrde.epita.fr/doxygen/group__tl__io.html), which prints formulas in SPIN format rather than in SPOT's native format (so [] instead of G, <> instead of F, and V instead of R, I believe). I did try some of the other print functions, but found none that print in SPOT's native format. For backwards compatibility, it would be better to find a printing function that prints in SPOT's native format, or write one custom.
The PR includes some code copied directly from SPOT, which poses a bit of a licensing issue, since SPOT is GPL 3.0 (requires all projects that integrate code from SPOT/include SPOT as a linked library to be GPL 3.0) as well, essentially preventing commercial use of Texada. Some of these code similarities are probably inevitable (e.g. the visitor pattern), but there is other copied code that I think brings in unneccessary complexity into the code base (e.g., the texadatospotformula includes some elements of SPOT formulas which I don't think Texada needs?)

This leaves us with 2 options:

We iterate on this PR to fix the tests remove the copied code from SPOT.
We integrate your changes into a SPOT 2.X support branch. We can change the test cases to show the new print behavior there. Later contributors can help us strip the copied SPOT code to integrate the support into main. Like this anyone who doesn't want a GPL 3.0 license/SPOT 2.X support can still use the main branch.

What do you think?

If 2., I will open a new SPOT 2.X support branch, and you can create a PR that targets that branch. I can help fix some of the formatting issues there.

cjbanks · 2022-02-04T22:07:47Z

I am happy with option 2 both for myself and users who do not plan to use Texada for commercial use. I think it is good to think about for future contributions.

If it were possible to iterate on the wrapper by moving the copied code to make an independent library and then have Texada depend on it seperately would this address the licencing issue? This would effectively have Texada depend on both SPOT and this "SPOT adjacent" library. I am not sure how easy it is to do though..

carolemieux · 2022-02-17T22:58:16Z

Sorry I'm being so slow on this!

So, I just made a new spot-2.x support branch. I think a few changes are needed before merging there:

update the tests so they pass
move all the formula stuff to a formula subdir in the source rather than in instantiation-tools
update the README.md and LICENSE doc accordingly.

I've done most of 2. and just need to check that everything builds, but if I'm taking too long just ping me here. After all that is done merge and close the PR, and I'll update the main README.md to point to this branch.

I don't think we should make another independent library that Texada depends on at this point. First I want to see how much of the copied code can be removed. I think we might be able to get rid of most of it:

for example, texada::formula right now supports all the operators that SPOT supports, but the texada checker does not really support those (bunop, for instance). So we could restructure texada::formula accordingly
we can also get rid of all the properties in texada::formula that are copied over from spot but we don't need (i.e. the ltl_prop stuff on line 67 of texadatospotformula.h, and all the comparison operators for formulas; do we need that lying around? On a quick check I don't think texada uses these)
I'm also not sure how much of the refformula stuff we need---really the clean thing would be to upgrade to smart pointers, (or just pass all the formula arguments as references?) and this should remove the need for reference counting at all.
Ideally from a software engineering perspective I'd like to decouple the spot formula from the texada formula, so that texada::formula doesn't carry around its own spot formula. It seems like the main place where we really need the spot formula is in the call to negative_normal_form, and the parsing/printing? Perhaps we would take a performance hit by not carrying around the spot formula, but I am not sure.

I think other than that, the primary borrowings from spot are the visitor pattern --- like the postfix visitor and clone visitor, correct? Code similarity is I think inevitable for such a standard pattern, and I think we should be able to simplify things to not need both the clone visitor and postfix visitor --- at that point the code will probably be fresh enough to not have these duplications issues. Is there anything else major I'm missing?

If you want to tackle some of these things, we can iterate on it (and I'll make the thoughts I outlined above more precise), but I figure we might as well incorporate your contribution now so that other users can take advantage of it. The refformula/ memory management stuff in particular seems like it could get hairy. What do you think?

…ools

carolemieux · 2022-03-08T22:13:58Z

Merged, thanks again for all the hard work adding this support :)

cjbanks · 2022-03-09T16:29:52Z

Thank you for the quick responses! Sorry I've been so behind on catching up to these messages..I'm glad the additions I made were useful. If I have time in a month or so I'd be happy to put a little more effort into addressing the main branch licencing issues. Thanks again!

cjbanks added 20 commits January 16, 2022 16:14

adds header files for common automata

4ea4d5e

adds mapping from SPOT 2.X atomic propositions to Texada calls

7826f9d

adds mapping from SPOT 2.X binop formulas to Texada calls

8a98dea

adds mapping from SPOT 2.X bunop formulas to Texada calls

02c39e9

adds mapping from SPOT 2.X constant functions to Texada calls

3ea39f6

makes an environment wrapper for Texada calls

11b10a6

adds mapping from SPOT 2.X multop formulas to Texada calls

912badf

adds mapping from SPOT 2.X unop formulas to Texada calls

c711a72

generates negative normal form formula from Texada formula

1bcc4f9

generates Texada simplifier wrapper around SPOT simplifier

f8c7bc3

adds postfix_visitor from SPOT 1.2.X to Texada to emulate visitors fr…

2f32c53

…om SPOT

adds pre-declaration of SPOT formula objects

a1f02f0

adds the main mapping/base class from SPOT 2.X formulas to Texada for…

f8ca09a

…mula calls

maps SPOT 2.X bindings to Texada functions. This is the main file for…

a67008f

… the wrapper

creates base class for formula class

55f87dd

creates visitor for Texada, SPOT no longer uses these for traversal

ed57a82

Namespace changes for instantiation-tools repo

7e6105a

Mapping files have updated the previous class/function calls to reside in texada namespace instead of spot since these calls may be defunct in SPOT 2.X

changes namespace calls for SPOT functions now in Texada

33b682a

Update checkers to use texada namespace for ltl

41741d8

Cannot use SPOT namespace with current object calls so we use the texada namespace and use the mappings created for Texada

updates the tests to use texada namespaces

9b61183

cjbanks changed the title ~~Issue 31: Added SPOT 2.X wrapper~~ Issue 31: Added SPOT 2.X wrapper #31 Jan 17, 2022

cjbanks changed the title ~~Issue 31: Added SPOT 2.X wrapper #31~~ Issue 31: Added SPOT 2.X wrapper Jan 17, 2022

cjbanks marked this pull request as ready for review January 17, 2022 21:29

carolemieux reviewed Jan 27, 2022

View reviewed changes

carolemieux changed the base branch from master to spot-2.x February 17, 2022 20:52

carolemieux added 5 commits February 18, 2022 14:51

move to std=c++17, because it's 2022

5c1bef8

move all of ltl::formula to a subdirectory other than instantiation t…

753f6bd

…ools

update test for SPIN format

ed0f430

Update README to reflect Spot 2.X support

21ff684

Update licenses

ce99f96

carolemieux merged commit 37a7356 into ModelInference:spot-2.x Mar 8, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Issue 31: Added SPOT 2.X wrapper #82

Issue 31: Added SPOT 2.X wrapper #82

cjbanks commented Jan 17, 2022

carolemieux commented Jan 19, 2022

carolemieux Jan 27, 2022

carolemieux Jan 27, 2022

cjbanks Feb 3, 2022

carolemieux Jan 27, 2022

cjbanks Feb 4, 2022

carolemieux Jan 27, 2022

carolemieux commented Jan 27, 2022

carolemieux commented Feb 1, 2022

cjbanks commented Feb 4, 2022

carolemieux commented Feb 17, 2022 •

edited

Loading

carolemieux commented Mar 8, 2022

cjbanks commented Mar 9, 2022

Issue 31: Added SPOT 2.X wrapper #82

Issue 31: Added SPOT 2.X wrapper #82

Conversation

cjbanks commented Jan 17, 2022

carolemieux commented Jan 19, 2022

carolemieux Jan 27, 2022

Choose a reason for hiding this comment

carolemieux Jan 27, 2022

Choose a reason for hiding this comment

cjbanks Feb 3, 2022

Choose a reason for hiding this comment

carolemieux Jan 27, 2022

Choose a reason for hiding this comment

cjbanks Feb 4, 2022

Choose a reason for hiding this comment

carolemieux Jan 27, 2022

Choose a reason for hiding this comment

carolemieux commented Jan 27, 2022

carolemieux commented Feb 1, 2022

cjbanks commented Feb 4, 2022

carolemieux commented Feb 17, 2022 • edited Loading

carolemieux commented Mar 8, 2022

cjbanks commented Mar 9, 2022

carolemieux commented Feb 17, 2022 •

edited

Loading