Skip to content

Commit

Permalink
Merge pull request #82 from cjbanks/Issue31
Browse files Browse the repository at this point in the history 
Merging the SPOT 2.X support into spot-2.x branch
  • Loading branch information
@carolemieux
carolemieux authored Mar 8, 2022
2 parents 3db1067 + ce99f96 commit 37a7356
Show file tree
Hide file tree
Showing 68 changed files with 3,516 additions and 661 deletions.
2 changes: 2 additions & 0 deletions LICENSE.md
View file
Original file line number Diff line number Diff line change
@@ -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

Expand Down
11 changes: 8 additions & 3 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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

Expand All @@ -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.

Expand All @@ -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:

Expand Down
2 changes: 1 addition & 1 deletion makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
78 changes: 39 additions & 39 deletions texada-src/src/checkers/boolbasedchecker.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand All @@ -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 {
Expand All @@ -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);
Expand All @@ -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,
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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) {
Expand All @@ -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++) {
Expand All @@ -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);
}
Expand Down
Loading

0 comments on commit 37a7356

Please sign in to comment.