Skip to content

Commit

Permalink
updated Interval
Browse files Browse the repository at this point in the history
  • Loading branch information
@MasWag
MasWag committed Oct 3, 2019
1 parent bba7228 commit 14a62a5
Show file tree
Hide file tree
Showing 5 changed files with 277 additions and 6 deletions.
4 changes: 3 additions & 1 deletion Doxyfile.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,6 @@ INPUT = @doxy_main_page@ \
FILE_PATTERNS = *.hh \
*.cc
RECURSIVE = YES
USE_MDFILE_AS_MAINPAGE = @doxy_main_page@
USE_MDFILE_AS_MAINPAGE = @doxy_main_page@
USE_MATHJAX = YES
EXTRACT_STATIC = YES
93 changes: 90 additions & 3 deletions libmonaa/interval.hh
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,69 @@
#pragma once
/*!
@file interval.hh
@author Masaki Waga
@brief The implementation of the class Interval and related functions
*/

#include <cmath>

#include "zone.hh"

/*!
@brief Class for an interval
*/
struct Interval {
Bounds lowerBound;
Bounds upperBound;

//! the lower bound of the interval
Bounds lowerBound;
//! the upper bound of the interval
Bounds upperBound;

/*!
@brief Defail constructor
By defalt the it returns the interval [0,∞)
*/
Interval() {
upperBound = Bounds{std::numeric_limits<double>::infinity(), false};
lowerBound = {0, true};
}

/*!
@brief Constructor returning the interval (lower, ∞)
@param [in] lower the lower bound
*/
Interval(int lower) {
upperBound = Bounds{std::numeric_limits<double>::infinity(), false};
lowerBound = {lower, false};
}

/*!
@brief Constructor returning the interval (lower, upper)
@param [in] lower the lower bound
@param [in] upper the upper bound
*/
Interval(int lower, int upper) {
upperBound = {upper, false};
lowerBound = {lower, false};
}

Interval(Bounds lower, Bounds upper) : lowerBound(lower), upperBound(upper){}

/*!
@brief The Kleene plus operator on intervals in [Dima'00]
For an interval \f$I\f$, the @em Kleen @em plus @em closure \f$I^+\f$ of \f$I\f$ is a set of intervals satisfying the following.
\f[
\bigcup_{i \in N} I^i = \bigcup_{I' \in I^+} I'
\f]
- [Dima'00]: Dima C. (2000) Real-Time Automata and the Kleene Algebra of Sets of Real Numbers. In: Reichel H., Tison S. (eds) STACS 2000. STACS 2000. Lecture Notes in Computer Science, vol 1770. Springer, Berlin, Heidelberg
@param [out] plusIntervals the result
*/
inline void plus(std::vector<std::shared_ptr<Interval>> &plusIntervals) {
plusIntervals.clear();
if (std::isinf(upperBound.first)) {
Expand All @@ -36,13 +81,25 @@ struct Interval {
}
};

//! @brief The intersection of two intervals
inline static Interval
operator&&( const Interval &left, const Interval &right) {
Interval ret = Interval{std::max(left.lowerBound, right.lowerBound),
std::min(left.upperBound, right.upperBound)};
return ret;
}

/*!
@brief The intersection of a set of intervals and an interval.
@note This function is destructive.
@param [in,out] left The set of intervals. We take intersection for each element of left and overwrite.
@param [in] right The interval.
We have the following relation between the input and the overwritten value of \f$\texttt{left}\f$.
\f[t \in \bigcup_{I \in \texttt{left}_{\mathrm{post}}} I \iff t \in \bigcup_{I \in \texttt{left}_{\mathrm{pre}}} (I \cap \texttt{right})\f]
*/
inline static void
land( std::vector<std::shared_ptr<Interval>> &left, const Interval &right) {
for (auto interval: left) {
Expand All @@ -53,11 +110,25 @@ land( std::vector<std::shared_ptr<Interval>> &left, const Interval &right) {
}), left.end());
}

/*!
@brief The intersection of two sets of intervals.
@note This function is destructive.
@param [in,out] left The set of intervals. We take intersection for each element of left and overwrite.
@param [in] right A set of interval. This is not overwritten.
We have the following relation between the input and the overwritten value of \f$\texttt{left}\f$.
\f[t \in \bigcup_{I \in \texttt{left}_{\mathrm{post}}} I \iff t \in \bigcup_{I \in \texttt{left}_{\mathrm{pre}}, I' \in \texttt{right}} (I \cap I')\f]
*/
inline static void
land( std::vector<std::shared_ptr<Interval>> &left, const std::vector<std::shared_ptr<Interval>> &right) {
std::vector<std::shared_ptr<Interval>> tmp;
for (auto interval: right) {
std::vector<std::shared_ptr<Interval>> tmpL = left;
for (auto &ptr: tmpL) {
ptr = std::make_shared<Interval>(*ptr);
}
land(tmpL, *interval);
tmp.insert(tmp.end(), tmpL.begin(), tmpL.end());
}
Expand All @@ -68,13 +139,29 @@ land( std::vector<std::shared_ptr<Interval>> &left, const std::vector<std::share
left = tmp;
}

/*!
@brief The sum of two intervals. The formal definition is as follows.
\f[I + I' = \{t + t' \mid \exists t \in I, t' \in I'\}\f]
*/
inline static Interval
operator+( Interval left, const Interval &right) {
left.lowerBound += right.lowerBound;
left.upperBound += right.upperBound;
return left;
}

/*!
@brief The sum of two sets of intervals.
@note This function is destructive.
@param [in,out] left The set of intervals. We take sum for each element of left and overwrite.
@param [in] right A set of interval. This is not overwritten.
We have the following for any \f$t \in \mathbb{R}\f$.
\f[t \in \bigcup_{I \in \texttt{left}_{\mathrm{post}}} I \iff \exists t' \in \bigcup_{I \in \texttt{left}_{\mathrm{pre}}}, \exists t'' \in \bigcup_{I' \in \texttt{right}}. t = t' + t'' \f]
*/
inline static void
operator+=( std::vector<std::shared_ptr<Interval>> &left, const std::vector<std::shared_ptr<Interval>> &right) {
std::vector<std::shared_ptr<Interval>> ans;
Expand Down
1 change: 1 addition & 0 deletions monaa/intermediate_tre.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ DNFTRE::DNFTRE(const std::shared_ptr<const TRE> tre) {
break;
}
case TRE::op::concat: {
// Flatten and concatenate
std::shared_ptr<DNFTRE> subfmlLeft = std::make_shared<DNFTRE>(tre->regExprPair.first);
std::shared_ptr<DNFTRE> subfmlRight = std::make_shared<DNFTRE>(tre->regExprPair.second);

Expand Down
89 changes: 87 additions & 2 deletions monaa/intermediate_tre.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,11 @@
#include "interval.hh"
#include "tre.hh"

/*!
@brief The syntactic decision of a DNFTRE or AtomicTRE
@todo Write what is the syntactic decision
*/
struct SyntacticDecision {
enum class Decision {
Constant,
Expand All @@ -15,9 +20,16 @@ struct SyntacticDecision {
std::vector<Alphabet> chars;
SyntacticDecision(const Decision &tag, const std::vector<Alphabet> &chars) : tag(tag), chars(chars) {}
void concat(std::shared_ptr<SyntacticDecision> in);
//! @brief Check if the decision is Mixed
inline bool isMixed() const {
return tag == Decision::Mixed && !chars.empty();
}
/*!
@brief Check if the decision is Constant
@param[out] singleC Write the constant value if the decision is Constant. Otherwise, it is not updated
@retval true if and only if the decision is Constant
*/
inline bool isConstant(char &singleC) {
if (chars.size() == 1) {
singleC = chars[0];
Expand All @@ -28,16 +40,50 @@ struct SyntacticDecision {
}
};

/*!
@brief A TRE of a single value
The signal value is defined by @link c @endlink and the length of the signal is represented by @link intervals @endlink.
Formally, we have the followng.
\f[
\sigma \in L(\varphi) \iff \exists I \in \mathtt{intervals}, t \in I. \sigma = \mathtt{c}^{t}
\f]
*/
class SingletonTRE {
public:
//! @brief The value of the TRE
Alphabet c;
//! @todo this is too naive implemenation. this must be slow.
/*!
@brief A set of intervals representing the length of the signals.
@note This is a naive implemenation. We can optimize the interval operations.
*/
std::vector<std::shared_ptr<Interval>> intervals;
/*!
@brief The constructor
@param [in] c The signal value
@param [in] intervals The length of the signals. If this is omitted, any length is accepted i.e., \f$ \mathtt{intervals} = [0,\infty)\f$.
*/
SingletonTRE(Alphabet c, std::vector<std::shared_ptr<Interval>> intervals = {std::make_shared<Interval>()}) : c(c), intervals(std::move(intervals)) {}
};

/*!
@brief A TRE without Boolean connectives (&& and ||) at the top-level or the children of the top-level within.
For example, the following expressions are atomic.
a, ab, (abc)%(1,4), (a|c)+
For example, the following expressions are NOT atomic.
a&&ab, (ab|c)%(1,4), a|c
*/
class AtomicTRE {
public:
//! @brief The top-level operation
enum class op {
singleton,
epsilon,
Expand All @@ -46,14 +92,23 @@ public:
within
};

//! @brief The constructor for \f$\varepsilon\f$
AtomicTRE() : tag(op::epsilon) {}
//! @brief The constructor for \f$c\f$ where \f$c \in \Sigma\f$
AtomicTRE(const Alphabet c) : tag(op::singleton), singleton(std::make_shared<SingletonTRE>(c)){}
//! @brief The constructor for a singleton TRE i.e., \f$\bigcup_{I \in \mathcal{I}} \langle c \rangle_{I} \f$ where \f$c \in \Sigma\f$
AtomicTRE(const std::shared_ptr<SingletonTRE> singleton) : tag(op::singleton), singleton(singleton) {}
//! @brief The constructor for a concatenation of three formulas
AtomicTRE(const std::list<std::shared_ptr<AtomicTRE>> &left, const std::shared_ptr<AtomicTRE> mid, const std::list<std::shared_ptr<AtomicTRE>> &right) : tag(op::concat), list() {
list = left;
list.push_back(mid);
list.insert(list.end(), right.begin(), right.end());
}
/*!
@brief The constructor for a concatenation of two formulas
@note Thanks to the optimization, the constructed formula may not be a concatenation e.g., an epsilon formula is given.
*/
AtomicTRE(const std::shared_ptr<AtomicTRE> left, const std::shared_ptr<AtomicTRE> right) : tag(op::concat), list() {
if (left->tag == op::concat) {
list = left->list;
Expand All @@ -65,8 +120,9 @@ public:
} else if (right->tag != op::epsilon) {
list.push_back(right);
}
// When the list is not concat anymore, use the original one
// Optimizatin: When the list is not concat anymore, use the original one
if (list.size() == 0) {
// list.size() == 0 <==> Both left and right are empty
tag = op::epsilon;
list.~list();
} else if (list.size() == 1) {
Expand Down Expand Up @@ -96,7 +152,9 @@ public:
}
}
}
//! @brief The constructor for the plus operator
AtomicTRE(const std::shared_ptr<DNFTRE> expr) : tag(op::plus), expr(expr) {}
//! @brief The constructor for the witin operator
AtomicTRE(const std::shared_ptr<AtomicTRE> atomic, const std::shared_ptr<Interval> interval) :tag (atomic->tag == op::singleton ? op::singleton : op::within) {
if (atomic->tag == op::singleton) {
new (&singleton) std::shared_ptr<SingletonTRE>(std::make_shared<SingletonTRE>(*(atomic->singleton)));
Expand All @@ -106,6 +164,7 @@ public:
}
}

//! @brief The destructer
~AtomicTRE() {
switch(tag) {
case op::epsilon:
Expand Down Expand Up @@ -133,20 +192,46 @@ public:
std::pair<std::shared_ptr<AtomicTRE>, std::shared_ptr<Interval>> within;
std::list<std::shared_ptr<AtomicTRE>> list;
};
//! @brief The SyntacticDecision for this AtomicTRE
std::shared_ptr<SyntacticDecision> decision;
//! @todo write what is the normal form
void toNormalForm();
//! @todo write what is the SNF
bool makeSNF(const char singleC);
void toSignalTA(TimedAutomaton& out) const;
};

/*!
@brief A timed regular expression of "DNF" form
The contained expression is
\f$\bigvee_{\Phi\in\texttt{list}} \bigwedge_{\varphi\in\Phi}\varphi\f$, where
\f$\varphi\f$ is an AtomicTRE.
@todo Masaki is writing here
*/
class DNFTRE {
public:
std::list<std::list<std::shared_ptr<AtomicTRE>>> list;
//! @brief the default constructor
DNFTRE() {}
/*!
@brief The constructor for \f$\bigwedge_{\varphi\in\texttt{conjunctions}}\varphi\f$, where
\f$\varphi\f$ is an AtomicTRE.
*/
DNFTRE(const std::list<std::shared_ptr<AtomicTRE>> &conjunctions) : list({conjunctions}){}
//! @brief Constricts a DNFTRE from TRE
DNFTRE(const std::shared_ptr<const TRE> tre);
//! @brief The SyntacticDecision for this DNFTRE
std::shared_ptr<SyntacticDecision> decision;
//! @todo write what is the normal form
void toNormalForm();
//! @todo write what is the SNF
bool makeSNF(const char singleC);
/*!
@brief Constract a signal timed automaton
@param [out] out The constructed (signal) timed automaton
*/
void toSignalTA(TimedAutomaton& out) const;
};

0 comments on commit 14a62a5

Please sign in to comment.