TeSSLa: TeSSLa Timed Dyadic Diontic Logic (TDDL) Library

module TDDL

TeSSLa implementation of Timed Dyadic Deontic Logic as presented here

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p1 = O("a", (Some(2), Some(4)))
def p2 = FC("b", "c", (Some(0), Some(6)), (Some(3), Some(5)))

def monitor = addToMonitor(Monitor(p1), p2)

def m1 = monitor(x)
def m2 = monitor(x)

out m1
out m2.dutySem

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
---
0: m1.rightSem = false
3: x = a
5: x = b
10: m1.dutySem = true
10: m2.dutySem = true

ANCHOR Type TDDLExpression

TDDLExpression[A]

TDDL Logical Expression.

ANCHOR Type TDDLInterval

TDDLInterval

Interval used in TDDL functions: (Option[Int], Option[Int]) Only positive intervals are supported. None at first position is equivalent to 0. None at the second position is equivalent to +inf.

ANCHOR Type TDDLMonitor

TDDLMonitor[A]

TDDL Monitor.

ANCHOR addToMonitor

addToMonitor[A](a: TDDLMonitor[A], exp: TDDLExpression[A]): TDDLMonitor[A]

Add a TDDL expression to a monitor

The monitor fulfilles the right semantics if any of its properties are fulfilled. The monitor fulfilles the duty semantics if all of its properties are fulfilled.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p1 = O("a", (Some(2), Some(4)))
def p2 = P("b", (Some(3), Some(5)))

def monitor = addToMonitor(Monitor(p1), p2)

def m1 = monitor(x)

out m1

option axis: true
option timeDomain: [-0.1,5]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
---
3: x = a
3: m1.dutySem = true
4: y = b
4: m1.rightSem = true

Source

def addToMonitor[A](a: TDDLMonitor[A], exp: TDDLExpression[A]) : TDDLMonitor[A] = {
  (inp: Events[A]) => {dutySem = TDDLUtils.finalAnd(a(inp).dutySem, exp.dutySem(TDDLUtils.time0, inp)), rightSem = TDDLUtils.finalOr(a(inp).rightSem, exp.rightSem(TDDLUtils.time0, inp))}
}

ANCHOR F

F[A](p: A, int: TDDLInterval): TDDLExpression[A]

Create a "Forbidden" expression that can be fed to a monitor.

p: The forbidden property. int: The interval in which the property is forbidden.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = F("a", (Some(2), Some(4)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
1: y = b
3: x = a
3: m1.dutySem = false
4: m2.dutySem = true
7: x = b
10: y = a

Source

def F[A](p: A, int: TDDLInterval): TDDLExpression[A] =
  {dutySem = TDDLDutySem.F(p, int), rightSem = TDDLRightSem.F(p, int)}

ANCHOR FC

FC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval): TDDLExpression[A]

Create a "Conditionally Forbidden" expression that can be fed to a monitor.

c: The condition property cint: The interval in which the condition activates the prohibition. p: The forbidden property. int: The interval in which the property is forbidden from the activation on.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = FC("a", "b", (Some(2), Some(4)), (Some(0), Some(2)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
2: x = a
3: y = a
3: x = b
3: m1.dutySem = false
5: m2.dutySem = true
7: x = b
10: y = a

Source

def FC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.FC(c, p, cint, pint), rightSem = TDDLRightSem.FC(c, p, cint, pint)}

ANCHOR Monitor

Monitor[A](exp: TDDLExpression[A]): TDDLMonitor[A]

Create a monitor from a TDDL expression

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p = O("a", (Some(2), Some(4)))

def monitor = Monitor(p)

def m1 = monitor(x)

out m1.dutySem

option axis: true
option timeDomain: [-0.1,5]
stream x: bubbles
stream m1.dutySem: signal
---
3: x = a
3: m1.dutySem = true

Source

def Monitor[A](exp: TDDLExpression[A]) : TDDLMonitor[A] = {
  (inp: Events[A]) => {dutySem = exp.dutySem(TDDLUtils.time0, inp), rightSem = exp.rightSem(TDDLUtils.time0, inp)}
}

ANCHOR O

O[A](p: A, int: TDDLInterval): TDDLExpression[A]

Create an "Obligated" expression that can be fed to a monitor.

p: The obligated property. int: The interval in which the property is obligated.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = O("a", (Some(2), Some(4)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
1: y = b
3: x = a
3: m1.dutySem = true
4: m2.dutySem = false
7: x = b
10: y = a

Source

def O[A](p: A, int: TDDLInterval): TDDLExpression[A] =
  {dutySem = TDDLDutySem.O(p, int), rightSem = TDDLRightSem.O(p, int)}

ANCHOR OC

OC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval): TDDLExpression[A]

Create a "Conditionally Obligated" expression that can be fed to a monitor.

c: The condition property cint: The interval in which the condition activates the obligation. p: The obligated property. int: The interval in which the property is obligated from the activation on.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = OC("a", "b", (Some(2), Some(4)), (Some(0), Some(2)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
2: x = a
3: y = a
3: x = b
3: m1.dutySem = true
5: m2.dutySem = false
7: x = b
10: y = a

Source

def OC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.OC(c, p, cint, pint), rightSem = TDDLRightSem.OC(c, p, cint, pint)}

ANCHOR Or

Or[A](a: TDDLExpression[A], b: TDDLExpression[A]): TDDLExpression[A]

Create a v (Disjunction) expression that can be fed to a monitor.

a: The first expression (lhs) b: The second expression (rhs)

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p = Or(O("a", (Some(2), Some(4))), O("b", (Some(0), Some(3))))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
2: y = b
2: m2.dutySem = true
3: x = a
3: m1.dutySem = true
7: x = 4
10: y = a

Source

def Or[A](a: TDDLExpression[A], b: TDDLExpression[A]) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.Or(a.dutySem, b.dutySem), rightSem = TDDLRightSem.Or(a.rightSem, b.rightSem)}

ANCHOR P

P[A](p: A, int: TDDLInterval): TDDLExpression[A]

Create a "Permitted" expression that can be fed to a monitor.

p: The permitted property. int: The interval in which the property is permitted.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = P("a", (Some(2), Some(4)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.dutySem = true
0: m2.dutySem = true
1: y = b
3: x = a
3: m1.rightSem = true
4: m2.rightSem = false
7: x = b
10: y = a

Source

def P[A](p: A, int: TDDLInterval): TDDLExpression[A] =
  {dutySem = TDDLDutySem.P(p, int), rightSem = TDDLRightSem.P(p, int)}

ANCHOR PC

PC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval): TDDLExpression[A]

Create a "Conditionally Permitted" expression that can be fed to a monitor.

c: The condition property cint: The interval in which the condition activates the permission. p: The permission property. int: The interval in which the property is permitted from the activation on.

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]
in y: Events[String]

def p = PC("a", "b", (Some(2), Some(4)), (Some(0), Some(2)))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.dutySem = true
0: m2.dutySem = true
2: x = a
3: x = b
3: m1.rightSem = true
4: m2.rightSem = false
7: x = b
10: y = a

Source

def PC[A](c: A, p: A, cint: TDDLInterval, pint: TDDLInterval) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.PC(c, p, cint, pint), rightSem = TDDLRightSem.PC(c, p, cint, pint)}

ANCHOR Pref

Pref[A](a: TDDLExpression[A], b: TDDLExpression[A]): TDDLExpression[A]

Create a » (Preference) expression that can be fed to a monitor.

a: The first expression (lhs) b: The second expression (rhs)

Generic type A is the type of the input stream.

Note this operator is not defined for the right semantics, hence the monitor will not generate right semantics output.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p = Pref(O("a", (Some(2), Some(4))), O("b", (Some(0), Some(3))))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m2.dutySem: signal
---
3: x = a
3: m1.dutySem = true
7: m2.dutySem = false
7: x = b
10: y = a

Source

def Pref[A](a: TDDLExpression[A], b: TDDLExpression[A]) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.Pref(a.dutySem, b.dutySem), rightSem = TDDLRightSem.Pref(a.rightSem, b.rightSem)}

ANCHOR Seq

Seq[A](a: TDDLExpression[A], b: TDDLExpression[A]): TDDLExpression[A]

Create a ; (Sequential) expression that can be fed to a monitor.

a: The first expression (lhs) b: The second expression (rhs)

Generic type A is the type of the input stream.

Usage:

include "TDDL.tessla"
import TDDL

in x: Events[String]

def p = Seq(O("a", (Some(2), Some(4))), O("b", (Some(0), Some(3))))

def monitor1 = Monitor(p)
def m1 = monitor(x)
out m1
def m2 = monitor(y)
out m2

option axis: true
option timeDomain: [-0.1,15]
stream x: bubbles
stream y: bubbles
stream m1.dutySem: signal
stream m1.rightSem: signal
stream m2.dutySem: signal
stream m2.rightSem: signal
---
0: m1.rightSem = false
0: m2.rightSem = false
3: x = a
4: m2.dutySem = false
5: x = b
5: m1.dutySem = true
10: y = a

Source

def Seq[A](a: TDDLExpression[A], b: TDDLExpression[A]) : TDDLExpression[A] =
  {dutySem = TDDLDutySem.Seq(a.dutySem, b.dutySem), rightSem = TDDLRightSem.Seq(a.rightSem, b.rightSem)}

TeSSLa Timed Dyadic Diontic Logic (TDDL) Library

Navigation

Source

Source

Source

Source

Source

Source

Source

Source

Source

Source

Source