! git clone https://github.com/MasWag/monaa.git

! apt install cmake libboost-dev flex libeigen3-dev doxygen bison -y

! mkdir -p monaa/build && cd monaa/build && cmake -DCMAKE_BUILD_TYPE=Release .. && make -j4  && make install

"""
Explanation: 1. Install MONAA
Download, build, and install  MONAA
End of explanation
"""


from typing import List

class MONAAResult:
    def __init__(self, raw_result:List[str]):
      self.lowerConstraint = raw_result[0].replace('t', 't, t')
      self.upperConstraint = raw_result[1].replace("t'", "t', t'")
      self.diffConstraint  = raw_result[2].replace("t' - t", "t'- t, t' - t")
    def __str__(self):
        return f'{self.lowerConstraint}, {self.upperConstraint}, {self.diffConstraint}'
    def __repr__(self):
        """
            This is not good. repr should return a valid python formula
        """
        return self.__str__()

import subprocess

def monaa(word:str = "", wordFile:str="", tre:str="", dot:str=""):
    if tre != "":
      if word != "":
        raw_result = subprocess.run(["monaa", "-e", tre], input=word, encoding='utf-8', stdout=subprocess.PIPE).stdout.strip().split('\n')
      elif wordFile != "":
        raw_result = subprocess.run(["monaa", "-e", tre, "-i", wordFile], encoding='utf-8', stdout=subprocess.PIPE).stdout.strip().split('\n')
      else:
        raise ValueError("Either word or wordFile must be given")
    elif dot != "":
      if word != "":
        raw_result = subprocess.run(["monaa", "-f", dot], input=word, encoding='utf-8', stdout=subprocess.PIPE).stdout.strip().split('\n')
      elif wordFile != "":
        raw_result = subprocess.run(["monaa", "-f", dot, "-i", wordFile], encoding='utf-8', stdout=subprocess.PIPE).stdout.strip().split('\n')
      else:
        raise ValueError("Either word or wordFile must be given")
    else:
      raise ValueError("Either tre or dot must be given")
    result = []
    for i in range(int(len(raw_result) / 4)):
      result.append(MONAAResult(raw_result[i*4:(i+1)*4]))
    return result                                          

import numpy as np
import matplotlib.pyplot as plt
import re

def plotConstr(constr:List[MONAAResult], lower, upper, cmap='Greys'):
    clockConstr = []
    d = np.linspace(lower, upper, 300)
    x,y = np.meshgrid(d,d)
    for singleZone in constr:
      tmpConstr = []
      for constrStr in str(singleZone).split(', '):
            tmpConstr.append('(' + constrStr.replace("t'", 'y').replace('t', 'x') + ')')
      clockConstr.append('(' + (' & '.join(tmpConstr)) + ')')
    plt.imshow( eval(' | '.join(clockConstr)).astype(int), 
               extent=(x.min(),x.max(),y.min(),y.max()),origin="lower", cmap=cmap, alpha = 0.3);

"""
Explanation: 2. Define the python wrapper
In this demo, we use the following python wrapper.
End of explanation
"""


!wget https://1drv.ws/u/s!AgmwSTftArYRjTWEsDTD1PTS75bS?e=fqmdUk

!tar xvf s!AgmwSTftArYRjTWEsDTD1PTS75bS\?e\=fqmdUk

"""
Explanation: 3. The velocity example
Let's try an example of timed pattern matching. Here, we detect sudden acceleration of a car. In this example we use the following TRE.
$(v < 30)\bigl\langle(v < 50)^*(v > 50)\$\bigr\rangle_{(0,50)}$
Intuitively, the specification means

At first, the velocity is less than or equal to 30
Then, the velocity keep less than or equal to 50
Finally, the velocity becomes greater than 50
The time gap between the initial $v < 50$ and the end of the trimming must be shorter than 5 time units.

3.1 The original log
We use the log generated from tprasadtp/cruise-control-simulink.
End of explanation
"""


!head data/10.0/BrCCPulse-120000.tsv

"""
Explanation: The logs are tsv files with the following fields.
 time   v(t)    v_ref(t)    |v(t) - v_ref(t)|
End of explanation
"""


!awk '$2 > 50{print "h", $1}$2 <= 50 && $2 > 30{print "m", $1} $2 <= 30{print "l", $1}' data/10.0/BrCCPulse-120000.tsv > /tmp/discrete.tsv

"""
Explanation: 3.2 Discretization of the log
Since we can use only Boolean propositions in timed pattern matching, we have to discretize the velocity in the log. Here, we use the following three propositions.

l: for $v \le 30$
m: for $30 < v \le 50$
h: for $50 < v$
End of explanation
"""


!head /tmp/discrete.tsv

"""
Explanation: The discretized log is as follows.
End of explanation
"""


result = monaa(wordFile='/tmp/discrete.tsv', tre='l((l|m)*h$)%(0,50)')
result[0:10]

"""
Explanation: 3.3 Result of timed pattern matching
The following is the initial 10 matching of timed pattern matching. It shows that the initial area of matching append around 450 -- 520 time units.
End of explanation
"""


!awk '$2 >= 450 && $2 <= 540{print $0}' /tmp/discrete.tsv

"""
Explanation: Indeed, we observe that the car suddenly accelerated at around 450--520 time units!!
End of explanation
"""


plotConstr(result[0:4], 450, 540)

"""
Explanation: The folowing 2-D plot illustrates the result.
End of explanation
"""


