Issue 31: Added SPOT 2.X wrapper

LICENSE.md

@@ -1,5 +1,7 @@
 Unless otherwise noted, projects in the Texada repository are
 distributed under the 3-clause BSD license, which appears below.
+Note that the code in the `texada-src/src/formula/` folder is 
+under a GPL 3.0 License, reproduced in that folder.  
 
 Copyright (c) 2018, University of British Columbia
 

README.md

@@ -44,6 +44,11 @@ Texada's output is a set of LTL formulae that are instantiations of the input pr
 
 As an example, consider the LTL property type that encodes the "x always followed by y" temporal relation between "x" and "y": G(x -> XF(y)). This property states that whenever an event of type "x" appears in a trace, it must be followed in the same trace by an event of type "y". Given an input log with two traces: "a,b,a,b,c" and "c,a,b,b", then Texada will output the property instantiations G(a -> XF(b)). That is, in the input two traces, "a is always followed by b".
 
+Two version of Texada are currently supported:
+* Texada with SPOT 1.2.4-1.2.6 support, which is in the `master` branch of this repository
+* Texada with SPOT 2.X support, which is in the `spot-2.x` branch of this repository. This version has two key differences:
+   - Code in the `texada-src/src/formula` directory is licensed under GPL-3.0.
+   - Formulas are output in [SPIN](http://spinroot.com/spin/Man/ltl.html) format; `[](a ->X<>(b))` rather than `G(a ->XF(b))`.
 
 # Installation guide
 
@@ -69,7 +74,7 @@ compiled all the commands you need to run to get started on [this wiki page](htt
 
 ### Required libraries
 
-Texada depends on a few non-standard libraries, [Google Test](https://code.google.com/p/googletest/), [SPOT](http://spot.lip6.fr/wiki/GetSpot), [Boost](http://www.boost.org/), and optionally [Z3](https://github.com/Z3Prover/z3). Note that the versions of SPOT currently compatible with Texada (1.2.4-1.2.6) also depend on BOOST.
+Texada depends on a few non-standard libraries, [Google Test](https://code.google.com/p/googletest/), [SPOT](http://spot.lip6.fr/wiki/GetSpot), [Boost](http://www.boost.org/), and optionally [Z3](https://github.com/Z3Prover/z3). 
 
 #### Google Test
 
@@ -85,7 +90,7 @@ To create a test, create a new Runner using 'Run As -> Run Configurations -> C/C
 
 #### Boost
 
-Boost can be downloaded [here](http://www.boost.org/doc/libs/1_56_0/more/getting_started/unix-variants.html) (for *nix machines) or [here](http://www.boost.org/doc/libs/1_56_0/more/getting_started/windows.html) (for Windows machines). Follow the instructions on the website to install it. Note that Texada depends on the non-header libraries, ProgramOptions and regex, which needs to be built separately (see "5. Prepare to Use a Boost Library Binary" on the Boost website). We have used Texada with BOOST versions 1.59.0-1.61.0.
+Boost can be downloaded [here](http://www.boost.org/doc/libs/1_56_0/more/getting_started/unix-variants.html) (for *nix machines) or [here](http://www.boost.org/doc/libs/1_56_0/more/getting_started/windows.html) (for Windows machines). Follow the instructions on the website to install it. Note that Texada depends on the non-header libraries, ProgramOptions and regex, which needs to be built separately (see "5. Prepare to Use a Boost Library Binary" on the Boost website). We have used Texada with BOOST versions 1.59.0-1.77.0.
 
 To integrate with Texada, the location of Boost headers will need to be inputted to uservars.mk (see "Building the project" below), so make note of where it is being extracted.
 
@@ -99,7 +104,7 @@ SPOT can be downloaded [here](http://spot.lip6.fr/wiki/GetSpot). Extract the fil
 
 To integrate with Texada, the location of SPOT headers and library will need to be inputted to uservars.mk (see "Building the project" below), so make note of where it is being extracted. 
 
-Texada currently is only compatible with Versions 1.2.4-1.2.6 of SPOT. Note that these versions require the installation of the [Boost](http://www.boost.org/) libraries. Its full functionality requires Python 2.0+ headers, but if these are not already installed, they can be omitted for the purposes of Texada. 
+The version of Texada in the `master` branch is compatible with SPOT 1.2.4-1.2.6, which is also dependent on BOOST. The version of Texada in the `spot-2.x` branch is compatible wiSPOT versions 2.X. 
 
 To install SPOT, navigate to the extracted SPOT folder and run these commands:
 

makefile

@@ -40,7 +40,7 @@ MAIN := texadamain
 SMTSET = 
 
 CC := g++
-CFLAGS = -std=c++11 -I$(SPOT_INCL) -I$(GTEST_INCL) -I$(BOOST_INCL) -O2 -g3 -Wall -c -fmessage-length=0 -MMD -MP -MF"$(@:%.o=%.d)" -MT"$(@:%.o=%.d)" -o "$@" "$<" 
+CFLAGS = -std=c++17 -I$(SPOT_INCL) -I$(GTEST_INCL) -I$(BOOST_INCL) -O2 -g3 -Wall -c -fmessage-length=0 -MMD -MP -MF"$(@:%.o=%.d)" -MT"$(@:%.o=%.d)" -o "$@" "$<" 
 
 # Add inputs and outputs from these tool invocations to the build variables 
 

texada-src/src/checkers/boolbasedchecker.h

@@ -12,7 +12,7 @@
 #include "statistic.h"
 #include "settings.h"
 #include "interval.h"
-#include "ltlvisit/tostring.hh"
+#include "../formula/texadatospotmapping.h"
 #include "../exceptions/unsupportedoperation.h"
 
 namespace texada {
@@ -73,10 +73,10 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic xor_check(const spot::ltl::binop *node, T trace_pt,
+        virtual statistic xor_check(const ltl::binop *node, T trace_pt,
                                     std::set<int> trace_ids) {
-            const spot::ltl::formula *p = node->first();
-            const spot::ltl::formula *q = node->second();
+            const ltl::formula *p = node->first();
+            const ltl::formula *q = node->second();
             statistic stat_p = this->check(p, trace_pt);
             statistic stat_q = this->check(q, trace_pt);
             statistic stat = statistic(true, 0, 0);
@@ -98,10 +98,10 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic equiv_check(const spot::ltl::binop *node,
+        virtual statistic equiv_check(const ltl::binop *node,
                                       T trace_pt, std::set<int> trace_ids) {
-            const spot::ltl::formula *p = node->first();
-            const spot::ltl::formula *q = node->second();
+            const ltl::formula *p = node->first();
+            const ltl::formula *q = node->second();
             statistic stat_p = this->check(p, trace_pt);
             statistic stat_q = this->check(q, trace_pt);
             statistic stat = statistic(true, 0, 0);
@@ -119,10 +119,10 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic implies_check(const spot::ltl::binop *node,
+        virtual statistic implies_check(const ltl::binop *node,
                                         T trace_pt, std::set<int> trace_ids) {
-            const spot::ltl::formula *p = node->first();
-            const spot::ltl::formula *q = node->second();
+            const ltl::formula *p = node->first();
+            const ltl::formula *q = node->second();
             if (!this->check(p, trace_pt).is_satisfied) {
                 return statistic(true, 0, 0);
             } else {
@@ -140,9 +140,9 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic not_check(const spot::ltl::unop *node, T trace_pt,
+        virtual statistic not_check(const ltl::unop *node, T trace_pt,
                                     std::set<int> trace_ids) {
-            const spot::ltl::formula *p = node->child();
+            const ltl::formula *p = node->child();
             statistic stat_p = this->check(p, trace_pt);
             if (stat_p.is_satisfied) {
                 return statistic(false, 0, 1);
@@ -160,7 +160,7 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic and_check(const spot::ltl::multop *node, T trace_pt,
+        virtual statistic and_check(const ltl::multop *node, T trace_pt,
                                     std::set<int> trace_ids) {
             int numkids = node->size();
             // In the case that the checker is configured to ignore statistics,
@@ -190,7 +190,7 @@ namespace texada {
          * @param trace_ids
          * @return
          */
-        virtual statistic or_check(const spot::ltl::multop *node, T trace_pt,
+        virtual statistic or_check(const ltl::multop *node, T trace_pt,
                                    std::set<int> trace_ids) {
             int numkids = node->size();
             // In the case that the checker is configured to ignore statistics,
@@ -257,43 +257,43 @@ namespace texada {
          * @param node the formula to find the interval of
          * @return
          */
-        virtual interval get_interval(const spot::ltl::formula *node) {
+        virtual interval get_interval(const ltl::formula *node) {
             switch (node->kind()) {
                 // interval(true) = interval(false) = interval(p) = [0,0]
-                case spot::ltl::formula::Constant:
-                case spot::ltl::formula::AtomicProp:
+                case ltl::formula::Constant:
+                case ltl::formula::AtomicProp:
                     return interval(0, 0);
 
-                case spot::ltl::formula::UnOp: {
-                    const spot::ltl::unop *unode = static_cast<const spot::ltl::unop *>(node);
+                case ltl::formula::UnOp: {
+                    const ltl::unop *unode = static_cast<const ltl::unop *>(node);
                     switch (unode->op()) {
                         // interval(Gp) = interval(Fp) = [0,inf+]
-                        case spot::ltl::unop::G:
-                        case spot::ltl::unop::F:
+                        case ltl::unop::G:
+                        case ltl::unop::F:
                             return interval(0, LONG_MAX);
                             // interval(Xp) = interval(p) + 1 (i.e. increment both the start and the end of interval(p))
-                        case spot::ltl::unop::X:
+                        case ltl::unop::X:
                             return get_interval(unode->child()) + 1;
                             // interval(Not(p)) = interval(p)
-                        case spot::ltl::unop::Not:
+                        case ltl::unop::Not:
                             return get_interval(unode->child());
                         default:
                             throw texada::unsupported_operation_exception("Unsupported unary operator.");
                     }
                 }
 
-                case spot::ltl::formula::BinOp: {
-                    const spot::ltl::binop *bnode = static_cast<const spot::ltl::binop *>(node);
+                case ltl::formula::BinOp: {
+                    const ltl::binop *bnode = static_cast<const ltl::binop *>(node);
                     switch (bnode->op()) {
                         // interval(pUq) = interval(pRq) = interval(pWq) = interval(pMq) = [0,inf+]
-                        case spot::ltl::binop::U:
-                        case spot::ltl::binop::R:
-                        case spot::ltl::binop::W:
-                        case spot::ltl::binop::M:
+                        case ltl::binop::U:
+                        case ltl::binop::R:
+                        case ltl::binop::W:
+                        case ltl::binop::M:
                             return interval(0, LONG_MAX);
-                        case spot::ltl::binop::Xor:
-                        case spot::ltl::binop::Equiv:
-                        case spot::ltl::binop::Implies: {
+                        case ltl::binop::Xor:
+                        case ltl::binop::Equiv:
+                        case ltl::binop::Implies: {
                             interval intvl(LONG_MAX, -LONG_MAX);
                             interval intvl_i = get_interval(bnode->first());
                             if (intvl.start > intvl_i.start) {
@@ -313,16 +313,16 @@ namespace texada {
                         }
 
                         default:
-                            throw texada::unsupported_operation_exception("Unsupported binary operator " + spot::ltl::to_string(node) + ".");
+                            throw texada::unsupported_operation_exception("Unsupported binary operator " + ltl::to_string(node) + ".");
                     }
                 }
 
-                case spot::ltl::formula::MultOp: {
-                    const spot::ltl::multop *mnode = static_cast<const spot::ltl::multop *>(node);
+                case ltl::formula::MultOp: {
+                    const ltl::multop *mnode = static_cast<const ltl::multop *>(node);
                     switch (mnode->op()) {
                         // interval(Or{p_i}) = interval(And{p_i}) = [a,b], where a = min{p_i.start} and b = max{p_i.end}
-                        case spot::ltl::multop::Or:
-                        case spot::ltl::multop::And: {
+                        case ltl::multop::Or:
+                        case ltl::multop::And: {
                             interval intvl(LONG_MAX, -LONG_MAX);
                             interval intvl_i;
                             for (int i = 0; i < mnode->size(); i++) {
@@ -341,8 +341,8 @@ namespace texada {
                     }
                 }
 
-                case spot::ltl::formula::BUnOp:
-                case spot::ltl::formula::AutomatOp:
+                case ltl::formula::BUnOp:
+                case ltl::formula::AutomatOp:
                 default:
                     return interval(-1, -1);
             }