Skip to content

Commit

Permalink
Minor improvement with ChainResponse/ChainPrecedence
Browse files Browse the repository at this point in the history
  • Loading branch information
@jackbergus
jackbergus committed Sep 2, 2023
1 parent 9a404b0 commit c1385d6
Show file tree
Hide file tree
Showing 20 changed files with 1,450 additions and 759 deletions.
2 changes: 2 additions & 0 deletions KnoBABQuery.g4
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,8 @@ ltlf : INIT TIMED? declare_arguments? declare_act_target?
| DIAMOND TIMED? ltlf #diamond
| NEGATED TIMED? ltlf PRESERVE? #not
| '(' ltlf ')' #paren
|<assoc=right> ltlf 'BX' THETA? INV? declare_arguments? declare_act_target? #and_next_B
|<assoc=right> ltlf 'XB' THETA? INV? declare_arguments? declare_act_target? #next_and_B
|<assoc=right> ltlf '&Ft' THETA? INV? ltlf #and_future
|<assoc=right> ltlf '&Ft!X' THETA? INV? ltlf #and_future_not_next
|<assoc=right> ltlf '&Ft!WX' THETA? INV? ltlf #and_wfuture_not_next
Expand Down
6 changes: 5 additions & 1 deletion include/knobab/server/algorithms/querymanager/LTLfQuery.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,9 @@ struct LTLfQuery {
LAST_QP = 17,
FALSEHOOD_QP = 18,
AFNXA_QPT = 19,
AFNWXA_QPT = 20
AFNWXA_QPT = 20,
AND_NEXT_QPT = 21,
NEXT_AND_QPT = 22,
};
bool doInvTheta = false;
type t;
Expand Down Expand Up @@ -114,6 +116,8 @@ struct LTLfQuery {
static LTLfQuery qDIAMOND(const LTLfQuery& lhs, bool isTimed);
static LTLfQuery qANDFUTURENOTNEXTA(const LTLfQuery& lhs, const LTLfQuery& rhs, bool isTimed, bool hasTheta, bool isInv);
static LTLfQuery qANDFUTURENOTWNEXTA(const LTLfQuery& lhs, const LTLfQuery& rhs, bool isTimed, bool hasTheta, bool isInv);
static LTLfQuery qANDNEXT(const LTLfQuery& lhs, short declare_argument, LeafType marking, bool isTimed, bool hasTheta, bool isInv);
static LTLfQuery qNEXTAND(const LTLfQuery& lhs, short declare_argument, LeafType marking, bool isTimed, bool hasTheta, bool isInv);
};


Expand Down
4 changes: 2 additions & 2 deletions include/knobab/server/algorithms/querymanager/MAXSatPipeline.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,8 +158,8 @@ struct MAXSatPipeline {
void data_chunk(CNFDeclareDataAware* model, const AtomizingPipeline& atomization, const KnowledgeBase& kb);
std::vector<PartialResult> subqueriesRunning(const KnowledgeBase &kb);
void abidinglogic_query_running(const std::vector<PartialResult>& results_cache, const KnowledgeBase& kb);
void fast_v1_query_running(const std::vector<PartialResult>& results_cache, const KnowledgeBase& kb);
void hybrid_query_running(const std::vector<PartialResult>& results_cache, const KnowledgeBase& kb);
void fast_v1_query_running(const std::vector<PartialResult>& results_cache, const AtomizingPipeline& ap, const KnowledgeBase& kb);
void hybrid_query_running(const std::vector<PartialResult>& results_cache, const AtomizingPipeline& ap, const KnowledgeBase& kb);
// LTLfQuery *pushAtomicQueries(const AtomizingPipeline &atomization, LTLfQuery *formula);

};
Expand Down
4 changes: 2 additions & 2 deletions include/knobab/server/declare/DeclareDataAware.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -165,9 +165,9 @@ struct DeclareDataAware {
bool compareAsThetaPredicate(const struct DeclareDataAware* ptr) const {
if (ptr == nullptr) return false;
return n == ptr->n
&& left_act == ptr->left_act
&& left_act == ptr->left_act && ptr->dnf_left_map == dnf_left_map
// && left_act_id == ptr->left_act_id
&& right_act == ptr->right_act
&& right_act == ptr->right_act && ptr->dnf_right_map == dnf_right_map
// && right_act_id == ptr->right_act_id
&& conjunctive_map == ptr->conjunctive_map;
}
Expand Down
103 changes: 90 additions & 13 deletions include/knobab/server/operators/novel_ltlf_operators.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,24 +7,62 @@
#ifndef KNOBAB_NOVEL_LTLF_OPERATORS_H
#define KNOBAB_NOVEL_LTLF_OPERATORS_H

#include <knobab/server/algorithms/atomization/AtomizingPipeline.h>
#include <knobab/server/tables/KnowledgeBase.h>

inline void and_next(const Result &lhsOperand,
Result& result,
const KnowledgeBase& kb,
act_t right_activity,
const PredicateManager* right_predicate = nullptr,
const AtomizingPipeline* ap,
const std::set<std::string>& rhs_atoms,
const PredicateManager* correlation = nullptr) {
std::unordered_set<std::string> cache;
if (right_predicate)
DEBUG_ASSERT(right_predicate->kb == &kb);
act_t right_activity;
bool right_predicate;
if ((!ap) ||((rhs_atoms.size() == 1) && ap->act_atoms.contains(*rhs_atoms.begin()))) {
right_predicate = false;
right_activity = kb.event_label_mapper.get(*rhs_atoms.begin());
} else {
right_predicate = true;
right_activity = kb.event_label_mapper.get(ap->atom_to_conjunctedPredicates.at(*rhs_atoms.begin()).at(0).label);
}
// if (right_predicate)
// DEBUG_ASSERT(right_predicate->kb == &kb);
for (const auto& x : lhsOperand) {
if ((kb.act_table_by_act_id.getTraceLength(x.first.first)-1) == (x.first.second))
continue;
size_t right_offset = kb.act_table_by_act_id.getBuilder().trace_id_to_event_id_to_offset.at(x.first.first).at(x.first.second+1);
if ((kb.act_table_by_act_id.table.at(right_offset).entry.id.parts.act != right_activity))
continue;
bool rightMatch = !right_predicate ? true : right_predicate->checkValidity(false, x.first.first, x.first.second);
bool rightMatch = true;
if (right_predicate) {
size_t table_offset =
kb.act_table_by_act_id.getBuilder().trace_id_to_event_id_to_offset.at(x.first.first).at(x.first.second+1);
for(const auto& pred_withConj : rhs_atoms){
bool result = true;
for (const auto& predDummy : ap->atom_to_conjunctedPredicates.at(pred_withConj)) {
bool test = true;
auto temp2_a = kb.attribute_name_to_table.find(predDummy.var);
if (temp2_a != kb.attribute_name_to_table.end()) {
std::optional<union_minimal> data = temp2_a->second.resolve_record_if_exists2(table_offset);
if (data.has_value()) {
if (!predDummy.testOverSingleVariable(data.value())) {
test = false;
}
}
}
if (!test) {
result = false;
break;
}
}
if (result) {
rightMatch= true;
break;
}
}
rightMatch= false;
}
if (rightMatch) {
if (correlation) {
env e1 = correlation->GetPayloadDataFromEvent(x.first.first, x.first.second, true, cache);
Expand All @@ -41,26 +79,65 @@ inline void and_next(const Result &lhsOperand,
inline void next_and(const Result &lhsOperand,
Result& result,
const KnowledgeBase& kb,
act_t right_activity,
const PredicateManager* right_predicate = nullptr,
const AtomizingPipeline* ap,
const std::set<std::string>& rhs_atoms,
const PredicateManager* correlation = nullptr) {
std::unordered_set<std::string> cache;
if (right_predicate)
DEBUG_ASSERT(right_predicate->kb == &kb);
act_t right_activity;
bool right_predicate;
if ((!ap) ||((rhs_atoms.size() == 1) && ap->act_atoms.contains(*rhs_atoms.begin()))) {
right_predicate = false;
right_activity = kb.event_label_mapper.get(*rhs_atoms.begin());
} else {
right_predicate = true;
right_activity = kb.event_label_mapper.get(ap->atom_to_conjunctedPredicates.at(*rhs_atoms.begin()).at(0).label);
}
for (const auto& x : lhsOperand) {
if (x.first.first == 0) continue;
if (x.first.second == 0) continue;
size_t right_offset = kb.act_table_by_act_id.getBuilder().trace_id_to_event_id_to_offset.at(x.first.first).at(x.first.second-1);
if ((kb.act_table_by_act_id.table.at(right_offset).entry.id.parts.act != right_activity))
continue;
bool rightMatch = !right_predicate ? true : right_predicate->checkValidity(false, x.first.first, x.first.second);
bool rightMatch = true;
if (right_predicate) {
size_t table_offset =
kb.act_table_by_act_id.getBuilder().trace_id_to_event_id_to_offset.at(x.first.first).at(x.first.second-1);
for(const auto& pred_withConj : rhs_atoms){
bool result = true;
for (const auto& predDummy : ap->atom_to_conjunctedPredicates.at(pred_withConj)) {
bool test = true;
auto temp2_a = kb.attribute_name_to_table.find(predDummy.var);
if (temp2_a != kb.attribute_name_to_table.end()) {
std::optional<union_minimal> data = temp2_a->second.resolve_record_if_exists2(table_offset);
if (data.has_value()) {
if (!predDummy.testOverSingleVariable(data.value())) {
test = false;
}
}
}
if (!test) {
result = false;
break;
}
}
if (result) {
rightMatch= true;
break;
}
}
rightMatch= false;
}
if (rightMatch) {
if (correlation) {
env e1 = correlation->GetPayloadDataFromEvent(x.first.first, x.first.second, true, cache);
if (correlation->checkValidity(e1, x.first.first, x.first.second-1)) {
result.emplace_back(x).second.second.emplace_back(marked_event::right(x.first.second-1));
auto& ref = result.emplace_back(x);
ref.first.second--;
ref.second.second.emplace_back(marked_event::right(x.first.second-1));
}
} else {
result.emplace_back(x).second.second.emplace_back(marked_event::right(x.first.second-1));
auto& ref = result.emplace_back(x);
ref.first.second--;
ref.second.second.emplace_back(marked_event::right(x.first.second-1));
}
}
}
Expand Down
6 changes: 6 additions & 0 deletions include/knobab/server/query_manager/KnoBABQueryBaseListener.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,9 @@ class KnoBABQueryBaseListener : public KnoBABQueryListener {
virtual void enterOr(KnoBABQueryParser::OrContext * /*ctx*/) override { }
virtual void exitOr(KnoBABQueryParser::OrContext * /*ctx*/) override { }

virtual void enterAnd_next_B(KnoBABQueryParser::And_next_BContext * /*ctx*/) override { }
virtual void exitAnd_next_B(KnoBABQueryParser::And_next_BContext * /*ctx*/) override { }

virtual void enterLast(KnoBABQueryParser::LastContext * /*ctx*/) override { }
virtual void exitLast(KnoBABQueryParser::LastContext * /*ctx*/) override { }

Expand Down Expand Up @@ -139,6 +142,9 @@ class KnoBABQueryBaseListener : public KnoBABQueryListener {
virtual void enterUntil(KnoBABQueryParser::UntilContext * /*ctx*/) override { }
virtual void exitUntil(KnoBABQueryParser::UntilContext * /*ctx*/) override { }

virtual void enterNext_and_B(KnoBABQueryParser::Next_and_BContext * /*ctx*/) override { }
virtual void exitNext_and_B(KnoBABQueryParser::Next_and_BContext * /*ctx*/) override { }

virtual void enterAnd_future(KnoBABQueryParser::And_futureContext * /*ctx*/) override { }
virtual void exitAnd_future(KnoBABQueryParser::And_futureContext * /*ctx*/) override { }

Expand Down
8 changes: 8 additions & 0 deletions include/knobab/server/query_manager/KnoBABQueryBaseVisitor.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,10 @@ class KnoBABQueryBaseVisitor : public KnoBABQueryVisitor {
return visitChildren(ctx);
}

virtual std::any visitAnd_next_B(KnoBABQueryParser::And_next_BContext *ctx) override {
return visitChildren(ctx);
}

virtual std::any visitLast(KnoBABQueryParser::LastContext *ctx) override {
return visitChildren(ctx);
}
Expand Down Expand Up @@ -179,6 +183,10 @@ class KnoBABQueryBaseVisitor : public KnoBABQueryVisitor {
return visitChildren(ctx);
}

virtual std::any visitNext_and_B(KnoBABQueryParser::Next_and_BContext *ctx) override {
return visitChildren(ctx);
}

virtual std::any visitAnd_future(KnoBABQueryParser::And_futureContext *ctx) override {
return visitChildren(ctx);
}
Expand Down
18 changes: 9 additions & 9 deletions include/knobab/server/query_manager/KnoBABQueryLexer.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,15 @@ class KnoBABQueryLexer : public antlr4::Lexer {
T__56 = 57, T__57 = 58, T__58 = 59, T__59 = 60, T__60 = 61, T__61 = 62,
T__62 = 63, T__63 = 64, T__64 = 65, T__65 = 66, T__66 = 67, T__67 = 68,
T__68 = 69, T__69 = 70, T__70 = 71, T__71 = 72, T__72 = 73, T__73 = 74,
VIOLATED = 75, VAC_SAT = 76, SAT = 77, ACT_TABLE = 78, WITH_ALIGNMENT_STRATEGY = 79,
CNT_TABLE = 80, ATT_TABLE = 81, ACTIVITYLABEL = 82, LOGS = 83, ATT = 84,
ACTIVATION = 85, TARGET = 86, INIT = 87, END = 88, EXISTS = 89, ABSENCE = 90,
NEXT = 91, OR = 92, AND = 93, FIRST = 94, LAST = 95, IF = 96, THEN = 97,
ELSE = 98, UNTIL = 99, BOX = 100, DIAMOND = 101, AUTO_TIMED = 102, LPAREN = 103,
RPAREN = 104, PRESERVE = 105, TIMED = 106, THETA = 107, LEFT = 108,
INV = 109, RIGHT = 110, MIDDLE = 111, NEGATED = 112, JOLLY = 113, HRF = 114,
TAB = 115, XES = 116, LABEL = 117, INTNUMBER = 118, NUMBER = 119, STRING = 120,
SPACE = 121, COMMENT = 122, LINE_COMMENT = 123
T__74 = 75, T__75 = 76, VIOLATED = 77, VAC_SAT = 78, SAT = 79, ACT_TABLE = 80,
WITH_ALIGNMENT_STRATEGY = 81, CNT_TABLE = 82, ATT_TABLE = 83, ACTIVITYLABEL = 84,
LOGS = 85, ATT = 86, ACTIVATION = 87, TARGET = 88, INIT = 89, END = 90,
EXISTS = 91, ABSENCE = 92, NEXT = 93, OR = 94, AND = 95, FIRST = 96,
LAST = 97, IF = 98, THEN = 99, ELSE = 100, UNTIL = 101, BOX = 102, DIAMOND = 103,
AUTO_TIMED = 104, LPAREN = 105, RPAREN = 106, PRESERVE = 107, TIMED = 108,
THETA = 109, LEFT = 110, INV = 111, RIGHT = 112, MIDDLE = 113, NEGATED = 114,
JOLLY = 115, HRF = 116, TAB = 117, XES = 118, LABEL = 119, INTNUMBER = 120,
NUMBER = 121, STRING = 122, SPACE = 123, COMMENT = 124, LINE_COMMENT = 125
};

explicit KnoBABQueryLexer(antlr4::CharStream *input);
Expand Down
6 changes: 6 additions & 0 deletions include/knobab/server/query_manager/KnoBABQueryListener.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,9 @@ class KnoBABQueryListener : public antlr4::tree::ParseTreeListener {
virtual void enterOr(KnoBABQueryParser::OrContext *ctx) = 0;
virtual void exitOr(KnoBABQueryParser::OrContext *ctx) = 0;

virtual void enterAnd_next_B(KnoBABQueryParser::And_next_BContext *ctx) = 0;
virtual void exitAnd_next_B(KnoBABQueryParser::And_next_BContext *ctx) = 0;

virtual void enterLast(KnoBABQueryParser::LastContext *ctx) = 0;
virtual void exitLast(KnoBABQueryParser::LastContext *ctx) = 0;

Expand Down Expand Up @@ -137,6 +140,9 @@ class KnoBABQueryListener : public antlr4::tree::ParseTreeListener {
virtual void enterUntil(KnoBABQueryParser::UntilContext *ctx) = 0;
virtual void exitUntil(KnoBABQueryParser::UntilContext *ctx) = 0;

virtual void enterNext_and_B(KnoBABQueryParser::Next_and_BContext *ctx) = 0;
virtual void exitNext_and_B(KnoBABQueryParser::Next_and_BContext *ctx) = 0;

virtual void enterAnd_future(KnoBABQueryParser::And_futureContext *ctx) = 0;
virtual void exitAnd_future(KnoBABQueryParser::And_futureContext *ctx) = 0;

Expand Down
48 changes: 39 additions & 9 deletions include/knobab/server/query_manager/KnoBABQueryParser.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,15 @@ class KnoBABQueryParser : public antlr4::Parser {
T__56 = 57, T__57 = 58, T__58 = 59, T__59 = 60, T__60 = 61, T__61 = 62,
T__62 = 63, T__63 = 64, T__64 = 65, T__65 = 66, T__66 = 67, T__67 = 68,
T__68 = 69, T__69 = 70, T__70 = 71, T__71 = 72, T__72 = 73, T__73 = 74,
VIOLATED = 75, VAC_SAT = 76, SAT = 77, ACT_TABLE = 78, WITH_ALIGNMENT_STRATEGY = 79,
CNT_TABLE = 80, ATT_TABLE = 81, ACTIVITYLABEL = 82, LOGS = 83, ATT = 84,
ACTIVATION = 85, TARGET = 86, INIT = 87, END = 88, EXISTS = 89, ABSENCE = 90,
NEXT = 91, OR = 92, AND = 93, FIRST = 94, LAST = 95, IF = 96, THEN = 97,
ELSE = 98, UNTIL = 99, BOX = 100, DIAMOND = 101, AUTO_TIMED = 102, LPAREN = 103,
RPAREN = 104, PRESERVE = 105, TIMED = 106, THETA = 107, LEFT = 108,
INV = 109, RIGHT = 110, MIDDLE = 111, NEGATED = 112, JOLLY = 113, HRF = 114,
TAB = 115, XES = 116, LABEL = 117, INTNUMBER = 118, NUMBER = 119, STRING = 120,
SPACE = 121, COMMENT = 122, LINE_COMMENT = 123
T__74 = 75, T__75 = 76, VIOLATED = 77, VAC_SAT = 78, SAT = 79, ACT_TABLE = 80,
WITH_ALIGNMENT_STRATEGY = 81, CNT_TABLE = 82, ATT_TABLE = 83, ACTIVITYLABEL = 84,
LOGS = 85, ATT = 86, ACTIVATION = 87, TARGET = 88, INIT = 89, END = 90,
EXISTS = 91, ABSENCE = 92, NEXT = 93, OR = 94, AND = 95, FIRST = 96,
LAST = 97, IF = 98, THEN = 99, ELSE = 100, UNTIL = 101, BOX = 102, DIAMOND = 103,
AUTO_TIMED = 104, LPAREN = 105, RPAREN = 106, PRESERVE = 107, TIMED = 108,
THETA = 109, LEFT = 110, INV = 111, RIGHT = 112, MIDDLE = 113, NEGATED = 114,
JOLLY = 115, HRF = 116, TAB = 117, XES = 118, LABEL = 119, INTNUMBER = 120,
NUMBER = 121, STRING = 122, SPACE = 123, COMMENT = 124, LINE_COMMENT = 125
};

enum {
Expand Down Expand Up @@ -603,6 +603,21 @@ class KnoBABQueryParser : public antlr4::Parser {
virtual std::any accept(antlr4::tree::ParseTreeVisitor *visitor) override;
};

class And_next_BContext : public LtlfContext {
public:
And_next_BContext(LtlfContext *ctx);

LtlfContext *ltlf();
antlr4::tree::TerminalNode *THETA();
antlr4::tree::TerminalNode *INV();
Declare_argumentsContext *declare_arguments();
Declare_act_targetContext *declare_act_target();
virtual void enterRule(antlr4::tree::ParseTreeListener *listener) override;
virtual void exitRule(antlr4::tree::ParseTreeListener *listener) override;

virtual std::any accept(antlr4::tree::ParseTreeVisitor *visitor) override;
};

class LastContext : public LtlfContext {
public:
LastContext(LtlfContext *ctx);
Expand Down Expand Up @@ -816,6 +831,21 @@ class KnoBABQueryParser : public antlr4::Parser {
virtual std::any accept(antlr4::tree::ParseTreeVisitor *visitor) override;
};

class Next_and_BContext : public LtlfContext {
public:
Next_and_BContext(LtlfContext *ctx);

LtlfContext *ltlf();
antlr4::tree::TerminalNode *THETA();
antlr4::tree::TerminalNode *INV();
Declare_argumentsContext *declare_arguments();
Declare_act_targetContext *declare_act_target();
virtual void enterRule(antlr4::tree::ParseTreeListener *listener) override;
virtual void exitRule(antlr4::tree::ParseTreeListener *listener) override;

virtual std::any accept(antlr4::tree::ParseTreeVisitor *visitor) override;
};

class And_futureContext : public LtlfContext {
public:
And_futureContext(LtlfContext *ctx);
Expand Down
4 changes: 4 additions & 0 deletions include/knobab/server/query_manager/KnoBABQueryVisitor.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,8 @@ class KnoBABQueryVisitor : public antlr4::tree::AbstractParseTreeVisitor {

virtual std::any visitOr(KnoBABQueryParser::OrContext *context) = 0;

virtual std::any visitAnd_next_B(KnoBABQueryParser::And_next_BContext *context) = 0;

virtual std::any visitLast(KnoBABQueryParser::LastContext *context) = 0;

virtual std::any visitAbsence(KnoBABQueryParser::AbsenceContext *context) = 0;
Expand Down Expand Up @@ -101,6 +103,8 @@ class KnoBABQueryVisitor : public antlr4::tree::AbstractParseTreeVisitor {

virtual std::any visitUntil(KnoBABQueryParser::UntilContext *context) = 0;

virtual std::any visitNext_and_B(KnoBABQueryParser::Next_and_BContext *context) = 0;

virtual std::any visitAnd_future(KnoBABQueryParser::And_futureContext *context) = 0;

virtual std::any visitFirst(KnoBABQueryParser::FirstContext *context) = 0;
Expand Down
2 changes: 2 additions & 0 deletions include/knobab/server/query_manager/ServerQueryManager.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,8 @@ class ServerQueryManager : public KnoBABQueryBaseVisitor {
std::any visitQuery_plan(KnoBABQueryParser::Query_planContext *context) override;
std::any visitAnd_future_not_next(KnoBABQueryParser::And_future_not_nextContext *ctx) override;
std::any visitAnd_wfuture_not_next(KnoBABQueryParser::And_wfuture_not_nextContext *ctx) override;
std::any visitAnd_next_B(KnoBABQueryParser::And_next_BContext *ctx) override;
std::any visitNext_and_B(KnoBABQueryParser::Next_and_BContext *ctx) override;

trace_visitor* tv = nullptr;
std::unordered_map<std::string, Environment> multiple_logs;
Expand Down
Loading

0 comments on commit c1385d6

Please sign in to comment.