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

Jump to bottom

Add test regular expression. #42

Merged
merged 3 commits into from
Apr 26, 2020
Merged

Add test regular expression. #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fe83133
add NNF transformer for TestRegExp.
marcofavorito Apr 26, 2020
2b8110c
add tests for Test regexp transformation.
marcofavorito Apr 26, 2020
a0e5f1f
fix regex in test name
marcofavorito Apr 26, 2020
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
34 changes: 31 additions & 3 deletions lib/include/atom_visitor.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,30 @@ class AtomsVisitor : public Visitor {
public:
static Logger logger;

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override{};
void visit(const LDLfAnd &) override{};
void visit(const LDLfOr &) override{};
void visit(const LDLfNot &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfDiamond<TestRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<TestRegExp> &x) override {
this->visit_temporal(x);
};

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override;
void visit(const TestRegExp &) override;

// callbacks for propositional logic
void visit(const PropositionalTrue &) override;
void visit(const PropositionalFalse &) override;
void visit(const PropositionalAtom &) override;
Expand All @@ -39,12 +63,16 @@ class AtomsVisitor : public Visitor {
void visit(const PropositionalNot &) override;

void visit(const QuotedFormula &) override{};
void visit(const Symbol &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &) override;
void visit(const LDLfBox<PropositionalRegExp> &) override;

template <class R> void inline visit_temporal(const LDLfTemporal<R> &x) {
result = apply(*x.get_regex());
auto y = apply(*x.get_formula());
result.insert(y.begin(), y.end());
}

set_atoms_ptr apply(const PropositionalFormula &b);
set_atoms_ptr apply(const LDLfFormula &b);
set_atoms_ptr apply(const RegExp &b);
};

set_atoms_ptr find_atoms(const LDLfFormula &);
Expand Down
1 change: 1 addition & 0 deletions lib/include/basic.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ enum TypeID {
t_LDLfDiamond,
t_LDLfBox,
t_PropositionalRegExp,
t_TestRegExp,
t_NFAState,
t_DFAState,
t_PropositionalTrue,
Expand Down
18 changes: 18 additions & 0 deletions lib/include/delta.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,13 +46,31 @@ class DeltaVisitor : public Visitor {
explicit DeltaVisitor(const set_atoms_ptr &prop_interpretation)
: prop_interpretation{prop_interpretation}, epsilon{false} {}

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
void visit(const LDLfDiamond<TestRegExp> &) override;
void visit(const LDLfBox<PropositionalRegExp> &x) override;
void visit(const LDLfBox<TestRegExp> &) override;
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};

void visit(const QuotedFormula &) override{};

std::shared_ptr<const PropositionalFormula> apply(const LDLfFormula &b);
};
Expand Down
55 changes: 48 additions & 7 deletions lib/include/logic.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,11 @@ class LDLfNot : public LDLfFormula {

// TODO consider template check "enable_if_t" vs static_assert in constructor
// template <class T, class=std::enable_if_t<std::is_base_of_v<RegExp, T>>>
template <class T> class LDLfTemporal : public LDLfFormula {
// template <class T>
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfTemporal : public LDLfFormula {
private:
const ldlf_ptr arg_;
const std::shared_ptr<const T> regex_;
Expand All @@ -123,6 +127,9 @@ template <class T> class LDLfTemporal : public LDLfFormula {
static_assert(std::is_base_of<RegExp, T>::value,
"concrete RegExp class not derived from RegExp");
}
explicit LDLfTemporal<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: regex_{std::dynamic_pointer_cast<const T>(regex)}, arg_{formula} {}
ldlf_ptr get_formula() const { return arg_; };
std::shared_ptr<const T> get_regex() const { return regex_; };
hash_t compute_hash_() const override {
Expand All @@ -133,7 +140,11 @@ template <class T> class LDLfTemporal : public LDLfFormula {
};
};

template <class T> class LDLfDiamond : public LDLfTemporal<T> {
// template <class T>
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfDiamond : public LDLfTemporal<T> {
public:
const static TypeID type_code_id = TypeID::t_LDLfDiamond;
bool is_canonical(const set_formulas &container_) const;
Expand All @@ -143,6 +154,11 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}
explicit LDLfDiamond<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}

bool is_equal(const Basic &o) const override {
return is_a<LDLfDiamond<T>>(o) and
Expand All @@ -160,12 +176,17 @@ template <class T> class LDLfDiamond : public LDLfTemporal<T> {
dynamic_cast<const LDLfDiamond &>(o).get_formula());
};
std::shared_ptr<const LDLfFormula> logical_not() const override {
return std::make_shared<LDLfBox<T>>(this->get_regex(),
this->get_formula()->logical_not());
// return std::make_shared<LDLfBox<T>>(this->get_regex(),
// this->get_formula()->logical_not());
return std::make_shared<LDLfDiamond<T>>(this->get_regex(),
this->get_formula()->logical_not());
};
};

template <class T> class LDLfBox : public LDLfTemporal<T> {
// template <typename T, typename = typename
// std::enable_if<std::is_base_of<RegExp, T>::value, T>::type>
// template <typename T, typename>
template <typename T> class LDLfBox : public LDLfTemporal<T> {
public:
const static TypeID type_code_id = TypeID::t_LDLfBox;
bool is_canonical(const set_formulas &container_) const;
Expand All @@ -175,6 +196,11 @@ template <class T> class LDLfBox : public LDLfTemporal<T> {
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}
explicit LDLfBox<T>(const std::shared_ptr<const RegExp> &regex,
const ldlf_ptr &formula)
: LDLfTemporal<T>(regex, formula) {
this->type_code_ = type_code_id;
}

bool is_equal(const Basic &o) const override {
return is_a<LDLfBox<T>>(o) and
Expand Down Expand Up @@ -205,15 +231,30 @@ class PropositionalRegExp : public RegExp {

public:
const static TypeID type_code_id = TypeID::t_PropositionalRegExp;
void accept(Visitor &v) const override{};
void accept(Visitor &v) const override;
explicit PropositionalRegExp(std::shared_ptr<const PropositionalFormula> f);
bool is_canonical(const set_formulas &container_) const;
bool is_canonical(const PropositionalFormula &f) const;
hash_t compute_hash_() const override;
std::shared_ptr<const PropositionalFormula> get_arg() const;
bool is_equal(const Basic &o) const override;
int compare(const Basic &o) const override;
};

class TestRegExp : public RegExp {
private:
const std::shared_ptr<const LDLfFormula> arg_;

public:
const static TypeID type_code_id = TypeID::t_TestRegExp;
void accept(Visitor &v) const override;
explicit TestRegExp(std::shared_ptr<const LDLfFormula> f);
bool is_canonical(const LDLfFormula &f) const;
hash_t compute_hash_() const override;
std::shared_ptr<const LDLfFormula> get_arg() const;
bool is_equal(const Basic &o) const override;
int compare(const Basic &o) const override;
};

class QuotedFormula : public Basic {
private:
protected:
Expand Down
51 changes: 46 additions & 5 deletions lib/include/nnf.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,20 +26,61 @@ namespace lydia {
class NNFTransformer : public Visitor {
private:
protected:
std::shared_ptr<LDLfFormula> result;
// TODO split into several transformers?
std::shared_ptr<const LDLfFormula> result;
std::shared_ptr<const RegExp> regex_result;

public:
// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &x) override;
void visit(const LDLfBox<PropositionalRegExp> &x) override;
std::shared_ptr<LDLfFormula> apply(const LDLfFormula &b);
void visit(const LDLfDiamond<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfDiamond<TestRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<PropositionalRegExp> &x) override {
this->visit_temporal(x);
};
void visit(const LDLfBox<TestRegExp> &x) override {
this->visit_temporal(x);
};

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override;
void visit(const TestRegExp &) override;

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};
Comment on lines +58 to +63
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we need these and the same for the other concrete visitors because now they are pure virtual methods in the abstract class, for better consistency.


void visit(const QuotedFormula &) override{};

std::shared_ptr<const LDLfFormula> apply(const LDLfFormula &b);
std::shared_ptr<const RegExp> apply(const RegExp &b);

template <typename T, typename = typename std::enable_if<
std::is_base_of<RegExp, T>::value, T>::type>
void inline visit_temporal(const LDLfTemporal<T> &x) {
if (x.type_code_ == TypeID::t_LDLfDiamond) {
result = std::make_shared<LDLfDiamond<T>>(apply(*x.get_regex()),
apply(*x.get_formula()));
} else if (x.type_code_ == TypeID::t_LDLfBox) {
result = std::make_shared<LDLfBox<T>>(apply(*x.get_regex()),
apply(*x.get_formula()));
}
}
};

std::shared_ptr<LDLfFormula> to_nnf(const LDLfFormula &);
std::shared_ptr<const LDLfFormula> to_nnf(const LDLfFormula &);

} // namespace lydia
} // namespace whitemech
21 changes: 21 additions & 0 deletions lib/include/propositional_logic.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,12 +128,33 @@ class EvalVisitor : public Visitor {
public:
explicit EvalVisitor(const set_atoms_ptr &interpretation)
: interpretation{interpretation} {};

// callbacks for LDLf
void visit(const Symbol &) override{};
void visit(const LDLfBooleanAtom &) override{};
void visit(const LDLfAnd &) override{};
void visit(const LDLfOr &) override{};
void visit(const LDLfNot &) override{};
void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
void visit(const LDLfDiamond<TestRegExp> &) override{};
void visit(const LDLfBox<PropositionalRegExp> &) override{};
void visit(const LDLfBox<TestRegExp> &) override{};
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override;
void visit(const PropositionalFalse &) override;
void visit(const PropositionalAtom &) override;
void visit(const PropositionalAnd &) override;
void visit(const PropositionalOr &) override;
void visit(const PropositionalNot &) override;

void visit(const QuotedFormula &) override{};

bool apply(const PropositionalFormula &b);
};

Expand Down
8 changes: 5 additions & 3 deletions lib/include/types.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,15 +29,17 @@ namespace lydia {

class Basic;
class Symbol;
class RegExp;
class LDLfFormula;
class LDLfBooleanAtom;
class LDLfAnd;
class LDLfOr;
class LDLfNot;
template <class T> class LDLfDiamond;
template <class T> class LDLfBox;
class RegExp;
class PropositionalRegExp;
class TestRegExp;
template <typename T> class LDLfTemporal;
template <typename T> class LDLfDiamond;
template <typename T> class LDLfBox;
class PropositionalFormula;
class PropositionalAtom;
class PropositionalTrue;
Expand Down
22 changes: 22 additions & 0 deletions lib/include/utils/print.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,12 +32,34 @@ class StrPrinter : public Visitor {
std::string result;

public:
// callbacks for LDLf
void visit(const Symbol &) override;
void visit(const LDLfBooleanAtom &) override;
void visit(const LDLfAnd &) override;
void visit(const LDLfOr &) override;
void visit(const LDLfNot &) override;
void visit(const LDLfDiamond<PropositionalRegExp> &) override{};
void visit(const LDLfDiamond<TestRegExp> &) override{};
void visit(const LDLfBox<PropositionalRegExp> &) override{};
void visit(const LDLfBox<TestRegExp> &) override{};
// TODO add all the combinations of temporal formulas + regular expression

// callbacks for regular expressions
void visit(const PropositionalRegExp &) override{};
void visit(const TestRegExp &) override{};

// callbacks for propositional logic
void visit(const PropositionalTrue &) override{};
void visit(const PropositionalFalse &) override{};
void visit(const PropositionalAtom &) override{};
void visit(const PropositionalAnd &) override{};
void visit(const PropositionalOr &) override{};
void visit(const PropositionalNot &) override{};

void visit(const QuotedFormula &) override{};

template <class T> void visit(const LDLfDiamond<T> &);

std::string apply(const vec_basic &v);
std::string apply(const set_formulas &v);
std::string apply(const Basic &b);
Expand Down
Loading