A Flink application project using Scala to implement Event-driven Interval Temporal Logic (eLTL) that extends Linear temporal logic LTL for analysing hybrid systems.
To run and test your application locally, you can just execute sbt run
then select the main class that contains the Flink job .
You can also package the application into a fat jar with sbt assembly
, then submit it as usual, with something like:
flink run -c org.example.WordCount /path/to/your/project/my-app/target/scala-2.11/testme-assembly-0.1-SNAPSHOT.jar
You can also run your application from within IntelliJ: select the classpath of the 'mainRunner' module in the run/debug configurations. Simply open 'Run -> Edit configurations...' and then select 'mainRunner' from the "Use classpath of module" dropbox.
- State formula p ∈ F evaluated on single states. An event e ∈ L is also a state formula
- Interval formula φ ∈ Φ, φ ∶ I → {true, f alse} describe the expected behaviour of continuous variables
- [tp, tq] ∈ I time intervals in which variables must be observed
- Event intervals [p, q], p, q ∈ F determine intervals of states in the trace
Given p, q ∈ F, and φ ∈ Φ, the formulae of eLTL logic are recursively constructed as follows:
ψ ∶∶= φ ∣ ¬ψ ∣ ψ1 ∨ ψ2 ∣ ψ1U[p,q]ψ2 ∣ ψ1Upψ2
The rest of the temporal operators are accordingly defined as:◇[p,q] ψ ≡ True U[p,q]ψ
◇p ψ ≡ True Up ψ
◻[p,q] ψ ≡ ¬(◇[p,q]¬ψ)
◻p ψ ≡ ¬(◇p ¬ψ)
│ build.sbt
├───csv
.
.
.
├───src
│ ├───main
.
.
.
│ │ │
│ │ └───scala
│ │ └───org
│ │ └───uma
│ │ Ejemplos.scala
│ │ eLTL.scala
│ │ Rendimiento.scala
│ │
│ └───test
│ └───scala
│ eLTLtest.scala
│ timeTest.scala
Operators | eLTL | Scala |
---|---|---|
Until | U | U |
Always | ◻ | A / A2 |
Eventually | ◇ | E / E2 |
Neg | ¬ | Neg |
Until | U | Or |
For all intervals that begin with "1" and end with "3" must contain at least one "2":
◻[p,q] ◇[r] True
p:{e==1}, q:{e==3} and r:{e==2}
The file csv/10.csv meets this condition, values are pairs with the forme (index: Long, Data: T), in this case T is an integer:1;1
2;0
3;0
4;0
5;2
6;0
7;0
8;0
9;0
10;3
Applying this formula the result has to give true:
...
override type T = (Long, Int)
type TT = Int
val path = os.pwd / "csv"
...
val _10 = benv.readCsvFile[T](path+"/10.csv", fieldDelimiter = ";")
...
def Start: (TT => Boolean) = (e: TT) => {e == 1}
def Stop : (TT => Boolean) = (e: TT) => {e == 3}
def Cond : (TT => Boolean) = (e: TT) => {e == 2}
...
println(A(Start, Stop) (E(Cond) (True)) (_10, 0, Long.MaxValue))
More examples have been implemented in Ejemplos.scala.
Check out this Jupyter notebook for more fun. https://github.com/AbuAwn/eLTL-master/blob/1.1/Rendimiento.ipynb