Update Texada to be compatible with SPOT 1.99.2

[bestchai]

SPOT 1.99.x seems to have substantially changed everything that was going on. While Texada can run on older versions of SPOT right now, it would be good to update it to be compatible with the newer versions of SPOT

[Issue created by carolemieux: 2015-08-19]

[cjbanks]

Hi, I'd like to help with this if possible! Are there preferred implementation instructions?

[carolemieux]

Oh, great!

I haven't looked at the code base (Texada or SPOT) for a while; looks like SPOT is now at version 2.9.7, so that is really the compatibility we should be aiming for.

The story as far as I can tell is that:
In between the version of SPOT with which I originally wrote Texada and 1.99.x+, there was some major refactoring of their API, replacing spot::ltl::formula with spot::formula. It also looks like newer versions of SPOT don't have subtypes of formula like spot::ltl::binop, which are used extensively in Texada (see this file, for examples). Instead, the spot::formula class provides a way to check the top operator of the formula.

I see a few avenues to go forward:

1. Updating the types in Texada to be compatible with the new spot::formula types, and any updates to accessors, etc. I would go with this but it looks like this may not be too straightforward given that there is no equivalent of spot::ltl::binop, etc., in the newer versions of SPOT. But this is just from my cursory look at the new SPOT; if you know a bit more about it, maybe this is the most straightforward way?
2. Refactoring to introduce a type hierarchy similar to the old spot::ltl::formula in Texada itself (i.e. texada:::ltl::formula, texada::ltl::binop,...), and back this by the new SPOT representation. Essentially this would be a wrapper around the SPOT representation. The nice thing with this is if you make the new type hierarchy similar to the old SPOT one, Texada's checking code wouldn't need to be touched. It would also actually open the door to entirely remove the dependence on SPOT. (We use it just for parsing LTL formula, rather than its more complicated automata capabilities)
3. Change the Texada code more drastically to be in line with the new SPOT: by this, I mean changing functions beyond their argument types and accessors for those types. I'm a little hesitant of any change that would require a radical change to the current Texada function interfaces, just for increased possibility of introducing bugs.

From my current look at things, I feel like 2. is the way to go, but if you think one of the other avenues (or some other option I haven't thought of) is better, happy to chat!

[bestchai]

+1 for option (2). The slightly further separation from SPOT will make Texada less likely to break whenever SPOT changes in the future.

[cjbanks]

Ok, I can work on the wrapper for Texada using option 2. Originally, I had planned to go with Option 1, but maybe for future compatibility I can go ahead with option 2. I am not entirely familiar with the old SPOT implementation but from what I can tell its a matter of creating namespaces within Texada and mapping the new SPOT properties to what is already referenced in Texada. There are quite a few updates in SPOT but I think the most important (for this application) is that formulas are now plain objects as oppossed to pointers. I don't think this should be an issue but I'll reach out if I have questions.

Also, for the type hierarchy would it be best to define within Texada a SPOT namespace as well (e.g. texada::spot::ltl:formula, etc.) in case new implementations for parsing LTL formulas are added?

[carolemieux]

Alright! Do get in touch if 2. is more onerous than it seems...

formulas are now plain objects as opposed to pointers
The place I imagine this having the most impact would be in the functions that do the instantiation of formulas with log events, but otherwise it shouldn't have too much of an impact.

Also, for the type hierarchy would it be best to define within Texada a SPOT namespace as well (e.g. texada::spot::ltl:formula, etc.) in case new implementations for parsing LTL formulas are added?
I would just go with texada::ltl::formula, I don't think we'll really need to separate new implementations for parsing LTL formulas.