Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Issue 31: Added SPOT 2.X wrapper #82

Merged
merged 25 commits into from
Mar 8, 2022
Merged

Issue 31: Added SPOT 2.X wrapper #82

Show file tree
Hide file tree
Changes from 20 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
4ea4d5e
adds header files for common automata
cjbanks Jan 16, 2022
7826f9d
adds mapping from SPOT 2.X atomic propositions to Texada calls
cjbanks Jan 16, 2022
8a98dea
adds mapping from SPOT 2.X binop formulas to Texada calls
cjbanks Jan 16, 2022
02c39e9
adds mapping from SPOT 2.X bunop formulas to Texada calls
cjbanks Jan 16, 2022
3ea39f6
adds mapping from SPOT 2.X constant functions to Texada calls
cjbanks Jan 16, 2022
11b10a6
makes an environment wrapper for Texada calls
cjbanks Jan 16, 2022
912badf
adds mapping from SPOT 2.X multop formulas to Texada calls
cjbanks Jan 16, 2022
c711a72
adds mapping from SPOT 2.X unop formulas to Texada calls
cjbanks Jan 16, 2022
1bcc4f9
generates negative normal form formula from Texada formula
cjbanks Jan 16, 2022
f8c7bc3
generates Texada simplifier wrapper around SPOT simplifier
cjbanks Jan 16, 2022
2f32c53
adds postfix_visitor from SPOT 1.2.X to Texada to emulate visitors fr…
cjbanks Jan 16, 2022
a1f02f0
adds pre-declaration of SPOT formula objects
cjbanks Jan 16, 2022
f8ca09a
adds the main mapping/base class from SPOT 2.X formulas to Texada for…
cjbanks Jan 16, 2022
a67008f
maps SPOT 2.X bindings to Texada functions. This is the main file for…
cjbanks Jan 16, 2022
55f87dd
creates base class for formula class
cjbanks Jan 16, 2022
ed57a82
creates visitor for Texada, SPOT no longer uses these for traversal
cjbanks Jan 16, 2022
7e6105a
Namespace changes for instantiation-tools repo
cjbanks Jan 16, 2022
33b682a
changes namespace calls for SPOT functions now in Texada
cjbanks Jan 16, 2022
41741d8
Update checkers to use texada namespace for ltl
cjbanks Jan 16, 2022
9b61183
updates the tests to use texada namespaces
cjbanks Jan 16, 2022
5c1bef8
move to std=c++17, because it's 2022
carolemieux Feb 18, 2022
753f6bd
move all of ltl::formula to a subdirectory other than instantiation t…
carolemieux Feb 18, 2022
ed0f430
update test for SPIN format
carolemieux Feb 18, 2022
21ff684
Update README to reflect Spot 2.X support
carolemieux Mar 4, 2022
ce99f96
Update licenses
carolemieux Mar 4, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 39 additions & 39 deletions texada-src/src/checkers/boolbasedchecker.h
View file
Open in desktop
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 "../instantiation-tools/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
57 changes: 28 additions & 29 deletions texada-src/src/checkers/lineartracechecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,8 @@
#include "boolbasedchecker.h"
#include "../instantiation-tools/apsubbingcloner.h"
#include "../instantiation-tools/pregeninstantspool.h"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/simplify.hh"
#include "tgba/bdddict.hh"
#include "../instantiation-tools/texadatospotmapping.h"
#include "../instantiation-tools/texadasimplify.h"
#include "statistic.h"
#include "settings.h"
namespace texada {
Expand All @@ -26,7 +25,7 @@ linear_trace_checker::linear_trace_checker(bool use_inv_s, shared_ptr<map<string
translations = ptr;
}

statistic linear_trace_checker::check_on_trace(const spot::ltl::formula * node, const event * trace){
statistic linear_trace_checker::check_on_trace(const ltl::formula * node, const event * trace){
return this->check(node, trace);
}

Expand All @@ -38,7 +37,7 @@ statistic linear_trace_checker::check_on_trace(const spot::ltl::formula * node,
* @param trace: pointer to the start of the trace
* @return whether node holds on trace
*/
statistic linear_trace_checker::ap_check(const spot::ltl::atomic_prop *node,
statistic linear_trace_checker::ap_check(const ltl::atomic_prop *node,
const event *trace, std::set<int> trace_ids) {
if (trace->is_satisfied(node->name())) {
return statistic(true, 1, 1);
Expand Down Expand Up @@ -67,10 +66,10 @@ statistic linear_trace_checker::ap_check(const spot::ltl::atomic_prop *node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::until_check(const spot::ltl::binop* node,
statistic linear_trace_checker::until_check(const ltl::binop* node,
const event* 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 cur_stat_p;
statistic cur_stat_q;
Expand Down Expand Up @@ -100,10 +99,10 @@ statistic linear_trace_checker::until_check(const spot::ltl::binop* node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::release_check(const spot::ltl::binop* node,
statistic linear_trace_checker::release_check(const ltl::binop* node,
const event* 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 cur_stat_p;
statistic cur_stat_q;
Expand Down Expand Up @@ -133,10 +132,10 @@ statistic linear_trace_checker::release_check(const spot::ltl::binop* node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::strongrelease_check(const spot::ltl::binop* node,
statistic linear_trace_checker::strongrelease_check(const ltl::binop* node,
const event* 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 cur_stat_p;
statistic cur_stat_q;
Expand Down Expand Up @@ -165,10 +164,10 @@ statistic linear_trace_checker::strongrelease_check(const spot::ltl::binop* node
* @param trace_ids
* @return
*/
statistic linear_trace_checker::weakuntil_check(const spot::ltl::binop* node,
statistic linear_trace_checker::weakuntil_check(const ltl::binop* node,
const event* 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 cur_stat_p;
statistic cur_stat_q;
Expand Down Expand Up @@ -201,9 +200,9 @@ statistic linear_trace_checker::weakuntil_check(const spot::ltl::binop* node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::globally_check(const spot::ltl::unop* node,
statistic linear_trace_checker::globally_check(const ltl::unop* node,
const event* trace_pt, std::set<int> trace_ids) {
const spot::ltl::formula * p = node->child();
const ltl::formula * p = node->child();

statistic cur_stat;
statistic ret_stat = statistic(true,0,0);
Expand Down Expand Up @@ -231,12 +230,11 @@ statistic linear_trace_checker::globally_check(const spot::ltl::unop* node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::finally_check(const spot::ltl::unop* node,
statistic linear_trace_checker::finally_check(const ltl::unop* node,
const event* trace_pt, std::set<int> trace_ids) {
const spot::ltl::formula * p = node->child();
const ltl::formula * p = node->child();

// TODO: why not combine the support, support pot here? (like in globally)

statistic cur_stat;
while (!trace_pt->is_terminal()){
if ((cur_stat = this->check(p,trace_pt)).is_satisfied){
Expand All @@ -259,9 +257,9 @@ statistic linear_trace_checker::finally_check(const spot::ltl::unop* node,
* @param trace_ids
* @return
*/
statistic linear_trace_checker::next_check(const spot::ltl::unop* node,
statistic linear_trace_checker::next_check(const ltl::unop* node,
const event* trace_pt, std::set<int> trace_ids) {
const spot::ltl::formula * p = node->child();
const ltl::formula * p = node->child();
// if we are at the terminal event, the next event is also a terminal
// event. Since we are traversing a finite tree, this will terminate.
if (trace_pt->is_terminal()) {
Expand All @@ -279,7 +277,7 @@ statistic linear_trace_checker::next_check(const spot::ltl::unop* node,
* @return
*/
vector<std::pair<map<string, string>, statistic>> valid_instants_on_traces(
const spot::ltl::formula * prop_type,
const ltl::formula * prop_type,
instants_pool_creator * instantiator,
shared_ptr<std::multiset<vector<event>>> traces,
bool use_invar_semantics,
Expand All @@ -298,7 +296,7 @@ vector<std::pair<map<string, string>, statistic>> valid_instants_on_traces(
* @return
*/
vector<std::pair<map<string, string>, statistic>> valid_instants_on_traces(
const spot::ltl::formula * prop_type,
const ltl::formula * prop_type,
instants_pool_creator * instantiator,
shared_ptr<std::multiset<vector<event>>> traces,
settings c_settings,
Expand All @@ -316,7 +314,7 @@ vector<std::pair<map<string, string>, statistic>> valid_instants_on_traces(
checker.configure(c_settings);
// simplifier for turning formulas into negative normal form so that
// statistics of formulae involving not, xor, <-> can be computed.
std::unique_ptr<spot::ltl::ltl_simplifier> simplifier(new spot::ltl::ltl_simplifier());
std::unique_ptr<ltl::ltl_simplifier> simplifier(new ltl::ltl_simplifier());

// Loop through each instantiation, filtering out those which are invalid (the notion of invalidity
// depending on the given checker settings).
Expand All @@ -329,16 +327,17 @@ vector<std::pair<map<string, string>, statistic>> valid_instants_on_traces(
if (current_instantiation == NULL) {
break;
}
const spot::ltl::formula * instantiated_prop_type = instantiate(prop_type,*current_instantiation,
const ltl::formula * instantiated_prop_type = instantiate(prop_type,*current_instantiation,
instantiator->get_events_to_exclude());
// unless checker is configured for the vanilla setting, turn formula into negative normal form.
// note that the the operators xor, <->, and -> will be reduced to basic operators by the below code.
if (!c_settings.is_vanilla()) {
// move original formula to a temp ptr to be destroyed
const spot::ltl::formula * to_delete = instantiated_prop_type;
const ltl::formula * to_delete = instantiated_prop_type;
instantiated_prop_type = simplifier->negative_normal_form(instantiated_prop_type);
to_delete->destroy();
}

// the meaning of validity will depend on the user inputed settings
bool valid = true;
statistic global_stat = statistic(true, 0, 0);
Expand Down
Loading