fourValuedLogicValue
Four valued logic value
AgeConstraint(events: Events[Int], maximum: Int, minimum: Int)
Checks the AgeConstraint as defined in the AUTOSAR Timing Extensions.
The events in the events streams must carry the age of the data, which is typically the point in time, when they were physically created.
Usage Example
in events: Events[Int]
def minimum: Int = 500
def maximum: Int = 900
def resetTime= 100
def constraint= AUTOSAR_TIMEX.ageConstraintReset(events, maximum, minimum, resetTime)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[600,750]
610: events = 100
610: constraint.value = true
610: constraint.final = false
620: events = 110
620: constraint.value = true
620: constraint.final = false
630: events = 120
630: constraint.value = true
630: constraint.final = false
640: events = 130
640: constraint.value = true
640: constraint.final = false
650: events = 140
650: constraint.value = true
650: constraint.final = false
660: events = 150
660: constraint.value = true
660: constraint.final = false
670: events = 160
670: constraint.value = true
670: constraint.final = false
680: events = 170
680: constraint.value = true
680: constraint.final = false
690: events = 180
690: constraint.value = true
690: constraint.final = false
700: events = 205
700: constraint.value = false
700: constraint.final = true
710: events = 200
710: constraint.value = false
710: constraint.final = true
720: events = 210
720: constraint.value = false
720: constraint.final = true
730: events = 220
730: constraint.value = false
730: constraint.final = true
def AgeConstraint(events: Events[Int], maximum: Int, minimum: Int):=
AgeConstraintReset(events, maximum, minimum, TADL2.pseudoInfty)AgeConstraintReset(events: Events[Int], maximum: Int, minimum: Int, resetTime: Int): Events[fourValuedLogicValue]
Checks the AgeConstraint as defined in the AUTOSAR Timing Extensions.
The events in the events streams must carry the age of the data, which is typically the point in time, when they were physically created.
A negative output is reset after resetTime.
see ageConstraint for a trace example.
def AgeConstraintReset(events: Events[Int], maximum: Int, minimum: Int, resetTime: Int): Events[fourValuedLogicValue]= {
def currentlyFulfilled(event: Events[Int], maximum: Int, minimum: Int): Events[Bool] =
events + minimum <= time(events) && events + maximum >= time(events)
TADL2.stillFulfillableReset(
if (currentlyFulfilled(events, maximum, minimum)) then
on(events, {value= true, final= false})
else
on(events, {value= false, final= true}),
resetTime)
}ArbitraryEventTriggering[A](events: Events[A], minDist: List[Int], maxDist: List[Int])
Checks the ArbitraryEventTriggering defined in TADL2.
The ArbitraryEventTriggering describes the time distances between several subsequent events
Usage Example
in x: Events[Unit]
def minDist: List[Int] := List.append(List.append(List.empty[Int], 1), 5)
def maxDist: List[Int] := List.append(List.append(List.empty[Int], 5), 6)
def constraint = AUTOSAR_TIMEX.ArbitraryEventTriggering(x, minDist, maxDist)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,48]
1: x = ()
1: constraint.value = true
1: constraint.final = false
6: x = ()
6: constraint.value = true
6: constraint.final = false
7: x = ()
7: constraint.value = true
7: constraint.final = false
11: x = ()
11: constraint.value = true
11: constraint.final = false
12: x = ()
12: constraint.value = true
12: constraint.final = false
16: x = ()
16: constraint.value = true
16: constraint.final = false
17: x = ()
17: constraint.value = true
17: constraint.final = false
21: x = ()
21: constraint.value = true
21: constraint.final = false
22: x = ()
22: constraint.value = true
22: constraint.final = false
26: x = ()
26: constraint.value = true
26: constraint.final = false
27: x = ()
27: constraint.value = true
27: constraint.final = false
31: x = ()
31: constraint.value = true
31: constraint.final = false
32: x = ()
32: constraint.value = true
32: constraint.final = false
36: x = ()
36: constraint.value = true
36: constraint.final = false
37: x = ()
37: constraint.value = true
37: constraint.final = false
41: x = ()
41: constraint.value = true
41: constraint.final = false
42: x = ()
42: constraint.value = true
42: constraint.final = false
46: x = ()
46: constraint.value = true
46: constraint.final = false
def ArbitraryEventTriggering[A](events: Events[A], minDist: List[Int], maxDist: List[Int]):=
TADL2.arbitraryConstraint(events, minDist, maxDist)ArbitraryEventTriggeringReset[A](events: Events[A], minDist: List[Int], maxDist: List[Int], resetTime: Int)
Checks the ArbitraryEventTriggering defined in TADL2.
resets a negative output after resetTime
see ArbitraryEventTriggeringReset for more information.
def ArbitraryEventTriggeringReset[A](events: Events[A], minDist: List[Int], maxDist: List[Int], resetTime: Int):=
TADL2.arbitraryConstraintReset(events, minDist, maxDist, resetTime)ConcretePatternEventTriggering[A](events: Events[A], patternLength: Int, offset: Map[Int, Int], patternPeriod: Int, patternJitter: Int)
checks the EventTriggeringConstraint.ConcretePatternEventTriggering defined in AUTOSAR Timex
The events for the must occur in a concretely given pattern given by offset, but a deviation is allowed, specified by the patternJitter attribute The entries of offset must be in ascending order (in keys and values) and the keys must start by 0. The patterns are repeating after patternPeriod.
The parameter patternLength does not play a role in monitoring, when patternPeriod is used.
Usage Example
in event: Events[Unit]
def patternPeriod = 20
def offset: Map[Int, Int] := Map.add(Map.add(Map.add(Map.empty[Int, Int], 0, 0), 1, 3), 2, 6)
def patternLength: Int = 6
def patternJitter: Int = 1
def constraint:= AUTOSAR_TIMEX.ConcretePatternEventTriggering(patternLength, offset, patternPeriod, patternJitter)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,60]
10: event = ()
10: constraint.value = true
10: constraint.final = false
13: event = ()
13: constraint.value = true
13: constraint.final = false
16: event = ()
16: constraint.value = true
16: constraint.final = false
31: event = ()
31: constraint.value = true
31: constraint.final = false
33: event = ()
33: constraint.value = true
33: constraint.final = false
36: event = ()
36: constraint.value = true
36: constraint.final = false
50: event = ()
50: constraint.value = true
50: constraint.final = false
53: event = ()
53: constraint.value = true
53: constraint.final = false
57: event = ()
57: constraint.value = true
57: constraint.final = false
def ConcretePatternEventTriggering[A](events: Events[A], patternLength: Int, offset: Map[Int, Int],
patternPeriod: Int, patternJitter: Int):=
ConcretePatternEventTriggeringReset(events, patternLength, offset, patternPeriod, patternJitter, TADL2.pseudoInfty)ConcretePatternEventTriggeringNoPeriod[A](events: Events[A], patternLength: Int, offset: Map[Int, Int])
checks the EventTriggeringConstraint.ConcretePatternEventTriggering defined in AUTOSAR Timex, without the use the parameter patternPeriod.
The events for the must occur in a concretely given pattern given by offset, but a deviation is allowed, specified by the patternJitter attribute The entries of offset must be in ascending order (in keys and values) and the keys must start by 0. The patterns are repeating after patternPeriod.
see ConcretePatternEventTriggering for more information.
def ConcretePatternEventTriggeringNoPeriod[A](events: Events[A], patternLength: Int, offset: Map[Int, Int]):=
ConcretePatternEventTriggering(events, patternLength, offset, patternLength, TADL2.pseudoInfty)ConcretePatternEventTriggeringNoPeriodReset[A](events: Events[A], patternLength: Int, offset: Map[Int, Int], resetTime: Int)
checks the EventTriggeringConstraint.ConcretePatternEventTriggering defined in AUTOSAR Timex, without the use the parameter patternPeriod.
resets a negative output after resetTime
see ConcretePatternEventTriggering for more information.
def ConcretePatternEventTriggeringNoPeriodReset[A](events: Events[A], patternLength: Int, offset: Map[Int, Int],
resetTime: Int):=
ConcretePatternEventTriggering(events, patternLength, offset, patternLength, TADL2.pseudoInfty)ConcretePatternEventTriggeringReset[A](events: Events[A], patternLength: Int, offset: Map[Int, Int], patternPeriod: Int, patternJitter: Int, resetTime: Int)
checks the EventTriggeringConstraint.ConcretePatternEventTriggering defined in AUTOSAR Timex
resets a negative output after resetTime
see ConcretePatternEventTriggering for more information.
def ConcretePatternEventTriggeringReset[A](events: Events[A], patternLength: Int, offset: Map[Int, Int],
patternPeriod: Int, patternJitter: Int, resetTime: Int):= {
liftable def aModuloBOr1if1(a: Int, b: Int): Int:=
if b == 1 then 1 else a % b;
def lowerBoundX: Events[Int] :=
if (last(res, events).final) then
on(events, 0)
else
merge (
# increase by period and adjust by offset and jitter
if (aModuloBOr1if1(TADL2.resetCount2(events, filter(events, last(res, events).final)), Map.size(offset))== 1 && !isFirst(events)) then
max(last(lowerBoundX, events) + patternPeriod,
time(events) - Map.get(offset,
(TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset))-patternJitter)
#adjust by offset and jitter
else
max(last(lowerBoundX, events),
time(events) - Map.get(offset,
(TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset))-patternJitter),
time(events) - Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset)) - patternJitter)
# lower bound for latest x
def upperBoundX: Events[Int] :=
if (last(res, events).final) then
on(events, TADL2.pseudoInfty)
else
merge (
# increase by period and adjust by offset and jitter
if (aModuloBOr1if1(TADL2.resetCount2(events, filter(events, last(res, events).final)), Map.size(offset))== 1 && !isFirst(events)) then
min(last(upperBoundX, events) + patternPeriod,
time(events) - Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset)))
else
# adjust by offset and jitter
min(last(upperBoundX, events),
time(events) - Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset))),
time(events) - Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset)))
# timestamps, in which the evaluation occurs
def evaluateTimes=
mergeUnit(events,
TADL2.safeDelay(upperBoundX + (if TADL2.resetCount2(events, filter(events, last(res, events).final)) % Map.size(offset) == 0 then
patternPeriod
else
0) +
Map.get(offset, TADL2.resetCount2(events, filter(events, last(res, events).final)) % Map.size(offset)) + patternJitter - time(events) + 1, events))
#evaluation
def res: Events[fourValuedLogicValue]= TADL2.stillFulfillableReset(merge(
# distance to x is correct-> current true, false otherwise
if (lowerBoundX +
Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset)) <=
time(evaluateTimes) &&
time(evaluateTimes) <= upperBoundX +
Map.get(offset, (TADL2.resetCount2(events, filter(events, last(res, events).final))-1) % Map.size(offset)) + patternJitter) then
{value= true, final= false}
else
{value= false, final= true},
{final= false, value = true}), resetTime)
res
}ExecutionOrderConstraintHierarchical(events: Events[Int], hierachicalOrder: Map[Int, List[Int]], resetTime: Int): Events[fourValuedLogicValue]
Checks the ExecutionOrderConstraint with ExecutionOrderConstraintType=hierachicalEOC as defined in the AUTOSAR-Timex Constraints
The events are identified by an unique identifier int-value, which must be given by the events-stream. The hierachical order is defined by the parameter hierachicalOrder. The keys of this map define the nodes in the hierachy-tree and the Values define childs of that.
Usage Example
in event: Events[Int]
def resetTime = 100
def hierachicalOrder: Map[Int, List[Int]] =
Map.add(Map.add(Map.add(Map.empty[Int, List[Int]], 1, List.append(List.append(List.empty[Int], 2), 3)), 2, List.append(List.append(List.empty[Int], 4), 5)), 3, List.append(List.append(List.empty[Int], 6), 7))
def constraint = ExecutionOrderConstraintHierarchical(event, hierachicalOrder, resetTime)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,37]
5: event = 1
5: constraint.final= false
5: constraint.value= true
10: event = 2
10: constraint.final= false
10: constraint.value= true
15: event = 4
15: constraint.final= false
15: constraint.value= true
20: event = 5
20: constraint.final= false
20: constraint.value= true
25: event = 3
25: constraint.final= false
25: constraint.value= true
30: event = 6
30: constraint.final= false
30: constraint.value= true
35: event = 7
35: constraint.final= true
35: constraint.value= true
def ExecutionOrderConstraintHierarchical(events: Events[Int], hierachicalOrder: Map[Int, List[Int]], resetTime: Int):
Events[fourValuedLogicValue]= {
# returns all event IDs, which are expected in hierachicalOrder
def allEvents(order: Map[Int, List[Int]], remainingKeys: List[Int]): Set[Int]:=
if (List.size(remainingKeys) == 0) then
Set.empty[Int]
else
# add element from directSuccesor-list
if List.size(Map.get(order, List.head(remainingKeys))) != 0 then
Set.add(allEvents(Map.add(order, List.head(remainingKeys),
List.tail(Map.get(order, List.head(remainingKeys)))), remainingKeys),
List.head(Map.get(order, List.head(remainingKeys))))
# direct successor list is empty-> use next event ID
else
Set.add(allEvents(order, List.tail(remainingKeys)), List.head(remainingKeys))
# determines those event IDs, which do not have a precondition (in general the root of the hierachical order tree (there can be multiple trees for this implementation))
def unboundedIDs(hierachicalOrder: Map[Int, List[Int]], remainingKeys: List[Int]): Set[Int]=
if (List.size(remainingKeys) == 0) then
allEvents(hierachicalOrder, Map.keys(hierachicalOrder))
else
removeListFromSet(unboundedIDs(hierachicalOrder, List.tail(remainingKeys)),
Map.get(hierachicalOrder, List.head(remainingKeys)))
# removes the current event from the expected events
liftable def removeCurrentEvent(expectedEvents: List[Set[Int]], events: Int):=
# current event not expected-> do nothing
if (List.size(expectedEvents) == 0 || !Set.contains(List.head(expectedEvents), events)) then
expectedEvents
else
deleteEmptyHead(List.prepend(Set.remove(List.head(expectedEvents), events), List.tail(expectedEvents)))
# List of sets of the expected events. The set in the head states, which events IDs are allowed for the next event
def nextEvents: Events[List[Set[Int]]]:= merge(list1(unboundedIDs(hierachicalOrder, Map.keys(hierachicalOrder))),
if (Map.contains(hierachicalOrder, events)) then
List.prepend(listToSet(Map.get(hierachicalOrder, events)), removeCurrentEvent(last(nextEvents, events), events))
else
removeCurrentEvent(last(nextEvents, events), events))
TADL2.stillFulfillableReset(
if List.size(last(nextEvents, events)) != 0 && Set.contains(List.head(last(nextEvents, events)), events) then
{final = false, value = true}
else
{final = true, value = false},
resetTime)
}ExecutionOrderConstraintOrdinary(events: Events[Int], linearOrder: List[Int], resetTime: Int): Events[fourValuedLogicValue]
Checks the ExecutionOrderConstraint with ExecutionOrderConstraintType=ordinarEOC as defined in the AUTOSAR-Timex Constraints
The events are identified by an unique identifier int-value, which must be given by the events-stream. The order of the events is given by the list linear order.
Usage Example
in event: Events[Int]
def resetTime = 100
def linearOrder: List[Int]= List.append(List.append(List.append(List.empty[Int], 7), 3), 5)
def constraint = ExecutionOrderConstraintLinear(event, linearOrder, resetTime)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,17]
5: event = 7
5: constraint.final= false
5: constraint.value= true
10: event = 3
10: constraint.final= false
10: constraint.value= true
15: event = 5
15: constraint.final= false
15: constraint.value= true
def ExecutionOrderConstraintOrdinary(events: Events[Int], linearOrder: List[Int], resetTime: Int):
Events[fourValuedLogicValue]= {
def hierarchicalFromLinearOrder(linOrder: List[Int]): Map[Int, List[Int]]:=
if (List.size(linOrder) == 0 || List.size(linOrder) == 1) then
Map.empty[Int, List[Int]]
else
Map.add(hierarchicalFromLinearOrder(List.tail(linOrder)),
List.head(linOrder), AUTOSAR_TIMEX.list1(List.head(List.tail(linOrder))))
ExecutionOrderConstraintHierarchical(events, hierarchicalFromLinearOrder(linearOrder), resetTime)
}ExecutionTimeConstraintGross[A, B](start: Events[A], end: Events[B], maximum: Int, minimum: Int): Events[fourValuedLogicValue]
Checks the ExecutionTimeConstraint with the parameter executionTimeType = gross as defined in the AUTOSAR Timing Extensions.
Checks, if the time between one start event and the next end event is between minimum and maximum. The events are expected to be in a logical order (start before end, …)
see ExecutionTimeConstraintNet for a trace example.
def ExecutionTimeConstraintGross[A, B](start: Events[A], end: Events[B], maximum: Int, minimum: Int):
Events[fourValuedLogicValue] :=
TADL2.executionTimeConstraint(start, end, 0, 0, minimum, maximum)ExecutionTimeConstraintGrossReset[A, B](start: Events[A], end: Events[B], maximum: Int, minimum: Int, resetTime: Int): Events[fourValuedLogicValue]
Checks the ExecutionTimeConstraint with the parameter executionTimeType = gross as defined in the AUTOSAR Timing Extensions.
Checks, if the time between one start event and the next end event is between minimum and maximum. The events are expected to be in a logical order (start before end, …)
A negative output is reset after resetTime.
see ExecutionTimeConstraintNet for a trace example.
def ExecutionTimeConstraintGrossReset[A, B](start: Events[A], end: Events[B], maximum: Int, minimum: Int, resetTime: Int):
Events[fourValuedLogicValue] :=
TADL2.executionTimeConstraintReset(start, end, 0, 0, minimum, maximum, resetTime)ExecutionTimeConstraintNet[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D], maximum: Int, minimum: Int): Events[fourValuedLogicValue]
Checks the ExecutionTimeConstraint with the parameter executionTimeType = net as defined in the AUTOSAR Timing Extensions.
Checks, if the time between one start event and the next end event, minus the preemptions, is between minimum and maximum. The events are expected to be in a logical order (start before end, preempt before resume, …)
Usage Example
in start: Events[Unit]
in end: Events[Unit]
in preempt: Events[Unit]
in resume: Events[Unit]
def lower = 10
def upper = 12
def constraint= TADL2.executionTimeConstraint(start, end, preempt, resume, 10, 12)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,22]
5: start = ()
5: constraint.value = true
5: constraint.final = false
10: preempt = ()
10: constraint.value = true
10: constraint.final = false
12: resume = ()
12: constraint.value = true
12: constraint.final = false
15: preempt = ()
15: constraint.value = true
15: constraint.final = false
17: resume = ()
17: constraint.value = true
17: constraint.final = false
20: end = ()
20: constraint.value = true
20: constraint.final = false
def ExecutionTimeConstraintNet[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D],
maximum: Int, minimum: Int): Events[fourValuedLogicValue] :=
TADL2.executionTimeConstraint(start, end, preempt, resume, minimum, maximum)ExecutionTimeConstraintNetReset[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D], maximum: Int, minimum: Int, resetTime: Int): Events[fourValuedLogicValue]
Checks the ExecutionTimeConstraint with the parameter executionTimeType = net as defined in the AUTOSAR Timing Extensions.
Checks, if the time between one start event and the next end event, minus the preemptions, is between minimum and maximum. The events are expected to be in a logical order (start before end, preempt before resume, …)
A negative output is reset after resetTime.
see ExecutionTimeConstraintNet for a trace example.
def ExecutionTimeConstraintNetReset[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D],
maximum: Int, minimum: Int, resetTime: Int): Events[fourValuedLogicValue] :=
TADL2.executionTimeConstraintReset(start, end, preempt, resume, minimum, maximum, resetTime)LatencyTimingConstraint(stimulus: Events[Int], response: Events[Int], isLatencyTypeAge: Bool, maximum: Int, minimum: Int, nominal: Int)
Checks the LatencyTimingConstraint defined in the Autosar Timing Extensions.
The LatencyConstraintType if set by isLatencyTypeAge (true-> LatencyConstraintType=age, false LatencyConstraintType->reaction)
If the LatencyConstraintType is age, there must one stimulus event for each reponse event within the specified time range earlier, which has the same color. If the LatencyConstraintType is reaction, after each stimulus event, there must be an event in the specified time range later in the response stream with the same color. The parameter resetTime specifies the time, after which a falsifying state should be deleted.
The Parameter nominal is unused in the monitoring Usage Example
in stimulus: Events[Int]
in response: Events[Int]
def minimum = 5
def maximum = 5
def nominal = 5
def isLatencyTypeAge = true
def resetTime = 100
def constraint= AUTOSAR_TIMEX.LatencyTimingConstraint(stimulus, response, isLatencyTypeAge, maximum, minimum, nominal, resetTime)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,25]
1: stimulus = 1
1: constraint.value = true
1: constraint.final = false
6: response = 1
6: constraint.value = true
6: constraint.final = false
8: stimulus = 4
8: constraint.value = true
8: constraint.final = false
10: stimulus = 2
10: constraint.value = true
10: constraint.final = false
13: stimulus = 3
13: constraint.value = true
13: constraint.final = false
15: response = 2
15: constraint.value = true
15: constraint.final = false
18: response = 3
18: constraint.value = true
18: constraint.final = false
def LatencyTimingConstraint(stimulus: Events[Int], response: Events[Int], isLatencyTypeAge: Bool,
maximum: Int, minimum: Int, nominal: Int):=
if (isLatencyTypeAge) then
TADL2.ageConstraint(stimulus, response, minimum, maximum)
else
TADL2.reactionConstraint(stimulus, response, minimum, maximum)LatencyTimingConstraintReset(stimulus: Events[Int], response: Events[Int], isLatencyTypeAge: Bool, maximum: Int, minimum: Int, nominal: Int, resetTime: Int)
Checks the LatencyTimingConstraint on individual events defined in the Autosar Timing Extensions.
resets a negative output after resetTime.
see LatencyTimingConstraint for more information.
def LatencyTimingConstraintReset(stimulus: Events[Int], response: Events[Int], isLatencyTypeAge: Bool,
maximum: Int, minimum: Int, nominal: Int, resetTime: Int):=
if (isLatencyTypeAge) then
TADL2.ageConstraintReset(stimulus, response, minimum, maximum, resetTime)
else
TADL2.reactionConstraintReset(stimulus, response, minimum, maximum, resetTime)OffsetTimingConstraint[A, B](source: Events[A], target: Events[B], maximum: Int, minimum: Int)
Checks the OffsetTimingConstraint as defined in the AUTOSAR Timing Extensions.
Each target event must be preceeded by a source event. The allowed time distance is defined by the maximum and the minimum parameter.
Usage Example
in source: Events[Unit]
in target: Events[Unit]
def minimum = 15
def maximum = 25
def resetTime = 100
def constraint= AUTOSAR_TIMEX.OffsetTimingConstraint(source, target, maximum, minimum)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,42]
5: source
5: constraint.value = true
5: constraint.final = false
10: source
10: constraint.value = true
10: constraint.final = false
15: source
15: constraint.value = true
15: constraint.final = false
20: source
20: target
20: constraint.value = true
20: constraint.final = false
25: source
25: target
25: constraint.value = true
25: constraint.final = false
30: source
30: target
30: constraint.value = true
30: constraint.final = false
35: source
35: target
35: constraint.value = true
35: constraint.final = false
40: source
40: target
40: constraint.value = true
40: constraint.final = false
def OffsetTimingConstraint[A, B](source: Events[A], target: Events[B], maximum: Int, minimum: Int):=
OffsetTimingConstraintReset(source, target, maximum, minimum, TADL2.pseudoInfty)OffsetTimingConstraintReset[A, B](source: Events[A], target: Events[B], maximum: Int, minimum: Int, resetTime: Int)
Checks the OffsetTimingConstraint as defined in the AUTOSAR Timing Extensions.
Each target event must be preceeded by a source event. The allowed time distance is defined by the maximum and the minimum parameter.
A negative Output is reset after resetTime.
see OffsetTimingConstraint for a trace example.
def OffsetTimingConstraintReset[A, B](source: Events[A], target: Events[B], maximum: Int, minimum: Int, resetTime: Int):= {
# remove all entries that are smaller than minVal from minVal
liftable def list_removeSmaller(list: List[Int], minVal: Int): List[Int]=
if (List.size(list) == 0) then
list
else
if (List.head(list) < minVal) then
list_removeSmaller(List.tail(list), minVal)
else
List.prepend(List.head(list), list_removeSmaller(List.tail(list), minVal))
# timestamps of stimulus events between now and maximum before that
def stimulusTimeStamps: Events[List[Int]]:= list_removeSmaller(
List.append(default(last(stimulusTimeStamps, source), List.empty[Int]), time(source)),
time(mergeUnit(source, target)) - maximum)
liftable def existsValidEvent(list: List[Int], absMin: Int, absMax: Int): Bool:=
if (List.size(list) == 0) then
false
else
(List.head(list) >= absMin && List.head(list) <= absMax) || existsValidEvent(List.tail(list), absMin, absMax)
def validTarget: Events[Bool]:= on(target, existsValidEvent(stimulusTimeStamps,
time(target) - maximum, time(target) - minimum))
def validSource: Events[Bool]:= on(source, true)
TADL2.stillFulfillableReset(
if merge(validTarget, validSource) then
{value= true, final= false}
else
{value= false, final= true},
resetTime)
}PeriodicEventTriggering[A](events: Events[A], patternPeriod: Int, jitter: Int, minInterArrivalTime: Int)
checks the EventTriggeringConstraint.PeriodicEventTriggering defined in AUTOSAR Timex
The events occur in a periodic pattern with an allowed deviation of jitter and a minimal distance of minInterArrivalTime.
Usage Example
in event: Events[Unit]
def patternPeriod = 10
def jitter = 2
def minInterArrivalTime = 9
def constraint= AUTOSAR_TIMEX.PeriodicEventTriggering(event, period, jitter, minInterArrivalTime)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,67]
5: event = ()
5: constraint.value = true
5: constraint.final = false
17: event = ()
17: constraint.value = true
17: constraint.final = false
26: event = ()
26: constraint.value = true
26: constraint.final = false
35: event = ()
35: constraint.value = true
35: constraint.final = false
47: event = ()
47: constraint.value = true
47: constraint.final = false
56: event = ()
56: constraint.value = true
56: constraint.final = false
65: event = ()
65: constraint.value = true
65: constraint.final = false
def PeriodicEventTriggering[A](events: Events[A], patternPeriod: Int, jitter: Int, minInterArrivalTime: Int):=
TADL2.periodicConstraint(events, patternPeriod, jitter, minInterArrivalTime)PeriodicEventTriggeringReset[A](events: Events[A], patternPeriod: Int, jitter: Int, minInterArrivalTime: Int, resetTime: Int)
checks the EventTriggeringConstraint.PeriodicEventTriggering defined in AUTOSAR Timex
A negative output is resetted after resetTime.
def PeriodicEventTriggeringReset[A](events: Events[A], patternPeriod: Int, jitter: Int,
minInterArrivalTime: Int, resetTime: Int):=
TADL2.periodicConstraintReset(events, patternPeriod, jitter, minInterArrivalTime, resetTime)sporadicEventTriggering[A](events: Events[A], jitter: Int, maxInterArrivalTime: Int, minInterArrivalTime: Int, patternPeriod: Int)
checks the EventTriggeringConstraint.sporadicEventTriggering defined in AUTOSAR Timex
The events occur in a periodic pattern, but less strict than in EventTriggeringConstraint.PeriodicEventTriggering defined. patternPeriod defines the nomimal, minInterArrivalTime the minimal and maxInterArrivalTime the maximal distance between subsequent events. jitter defines the allowed deviation from the periods.
Note that the definition of EventTriggeringConstraint.sporadicEventTriggering left room for different interpretations. This implementation uses the exact definition of Timmo-2-Use SporadicConstraint as interpretation.
Usage Example
in event: Events[Unit]
def patternPeriod = 10
def maxInterArrivalTime = 15
def jitter = 0
def minInterArrivalTime = 11
def constraint= AUTOSAR_TIMEX.sporadicEventTriggering(event, jitter, maxInterArrivalTime, minInterArrivalTime, patternPeriod)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,50]
5: event = ()
5: constraint.value = true
5: constraint.final = false
20: event = ()
20: constraint.value = true
20: constraint.final = false
31: event = ()
31: constraint.value = true
31: constraint.final = false
45: event = ()
45: constraint.value = true
45: constraint.final = false
def sporadicEventTriggering[A](events: Events[A], jitter: Int, maxInterArrivalTime: Int, minInterArrivalTime: Int,
patternPeriod: Int):=
TADL2.sporadicConstraint (events, patternPeriod, maxInterArrivalTime, jitter, minInterArrivalTime)sporadicEventTriggeringReset[A](events: Events[A], jitter: Int, maxInterArrivalTime: Int, minInterArrivalTime: Int, patternPeriod: Int, resetTime: Int)
checks the EventTriggeringConstraint.sporadicEventTriggering defined in AUTOSAR Timex a negative output is resetted after resetTime
See sporadicEventTriggering for more information
def sporadicEventTriggeringReset[A](events: Events[A], jitter: Int, maxInterArrivalTime: Int, minInterArrivalTime: Int,
patternPeriod: Int, resetTime: Int):=
TADL2.sporadicConstraintReset(events, patternPeriod, maxInterArrivalTime, jitter, minInterArrivalTime, resetTime)SynchronizationTimingConstraintEvents(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int, multipleOccurrences: Bool)
Checks the SynchronizationTimingConstraint on individual events defined in the Autosar Timing Extensions.
The SynchronizationTimingConstraint on events describes groups of streams, which events occur in common clusters. If the parameter multipleOccurrences is true, each of these streams must have at least one event in each of these intervals. If the parameter multipleOccurrences is false, each of these streams must have exactly one event in each of these intervals. The parameter tolerance specifies the maximal length of these intervals.
The events of each input timestamp must be placed into an integer list, which contains the index (starting at 1) of all streams, which have an event in this timestamp. This list is then used as a parameter for the implementation.
Usage Example
in event1: Events[Unit]
in event2: Events[Unit]
in event3: Events[Unit]
def timeNow: Events[Int] := time(mergeUnit(mergeUnit(events1, events2), events3))
def eventList3:=
if (defaultTime(events3) >= timeNow) then
List.prepend(3, List.empty[Int])
else
List.empty[Int]
def eventList2:=
if (defaultTime(events2) >= timeNow) then
List.prepend(2, eventList3)
else
eventList3
def eventList:=
if (defaultTime(events1) >= timeNow) then
List.prepend(1, eventList2)
else
eventList2
def tolerance = 2
def streamCount = 3
def multipleOccurrences = true
def constraint= SynchronizationTimingConstraintEvents(eventList, streamCount, tolerance, multipleOccurrences)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,50]
5: event1 = ()
5: event2 = ()
5: event3 = ()
5: constraint.value = true
5: constraint.final = false
15: event1 = ()
15: event2 = ()
15: event3 = ()
15: constraint.value = true
15: constraint.final = false
24: event1 = ()
24: constraint.value = false
24: constraint.final = false
25: event2 = ()
25: constraint.value = false
25: constraint.final = false
26: event3 = ()
26: constraint.value = true
26: constraint.final = false
34: event2 = ()
34: constraint.value = false
34: constraint.final = false
35: event3 = ()
35: constraint.value = false
35: constraint.final = false
36: event1 = ()
36: constraint.value = true
36: constraint.final = false
def SynchronizationTimingConstraintEvents(eventIndices: Events[List[Int]], streamCount: Int,
tolerance : Int, multipleOccurrences: Bool):=
if (multipleOccurrences) then
TADL2.synchronizationConstraintReset(eventIndices, streamCount, tolerance, TADL2.pseudoInfty)
else
TADL2.StrongSynchronizationConstraintReset(eventIndices, streamCount, tolerance, TADL2.pseudoInfty)SynchronizationTimingConstraintEventsMultiple(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int)
Checks the SynchronizationTimingConstraint on individual events defined in the Autosar Timing Extensions with EventOccurrenceKind = MultipleOccurrences
see SynchronizationTimingConstraintEvents for more information.
def SynchronizationTimingConstraintEventsMultiple(eventIndices: Events[List[Int]], streamCount: Int,
tolerance : Int):=
TADL2.synchronizationConstraintReset(eventIndices, streamCount, tolerance, TADL2.pseudoInfty)SynchronizationTimingConstraintEventsReset(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int, multipleOccurrences: Bool, resetTime: Int)
Checks the SynchronizationTimingConstraint on individual events defined in the Autosar Timing Extensions.
resets a negative output after resetTime.
see SynchronizationTimingConstraintEvents for more information.
def SynchronizationTimingConstraintEventsReset(eventIndices: Events[List[Int]], streamCount: Int,
tolerance : Int, multipleOccurrences: Bool, resetTime: Int):=
if (multipleOccurrences) then
TADL2.synchronizationConstraintReset(eventIndices, streamCount, tolerance, resetTime)
else
TADL2.StrongSynchronizationConstraintReset(eventIndices, streamCount, tolerance, resetTime)SynchronizationTimingConstraintEventsSingle(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int)
Checks the SynchronizationTimingConstraint on individual events defined in the Autosar Timing Extensions with EventOccurrenceKind = SingleOccurrences
see SynchronizationTimingConstraintEvents for more information.
def SynchronizationTimingConstraintEventsSingle(eventIndices: Events[List[Int]], streamCount: Int,
tolerance : Int):=
TADL2.StrongSynchronizationConstraintReset(eventIndices, streamCount, tolerance, TADL2.pseudoInfty)SynchronizationTimingConstraintResponseSynchronization(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType responseSynchronization as defined in the Autosar Timing Extensions.
The SynchronizationTimingConstraint on event chains for the synchronizationConstraintType responseSynchronization describes groups of streams, which response events occur in common clusters. The parameter tolerance specifies the maximal length of these intervals. If the parameter multipleOccurrences is true, each of these streams must have at least one event in each of these intervals. If the parameter multipleOccurrences is false, each of these streams must have exactly one event in each of these intervals.
Usage Example
in stimulus: Events[Int]
in response1: Events[Int]
in response2: Events[Int]
in response3: Events[Int]
def tolerance = 2
def timeNow =
merge(time(stimulus),
merge(time(response1),
merge(time(response2),
time(response3))))
def eventStimulus:= if (defaultTime(stimulus) >= timeNow) then Map.add(Map.empty[Int, Int], 0, default(stimulus, -1)) else Map.empty[Int, Int]
def eventResponse1:= if (defaultTime(response1) >= timeNow) then Map.add(eventStimulus, 1, default(response1, -1)) else eventStimulus
def eventResponse2:= if (defaultTime(response2) >= timeNow) then Map.add(eventResponse1, 2, default(response2, -1)) else eventResponse1
def eventResponse3:= if (defaultTime(response3) >= timeNow) then Map.add(eventResponse2, 3, default(response3, -1)) else eventResponse2
def responseStreamCount = 3
def multipleOccurrences = false
def constraint= AUTOSAR_TIMEX.SynchronizationTimingConstraintResponseSynchronization(eventResponse3, responseStreamCount, tolerance, multipleOccurrences)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,20]
1: stimulus = 1
1: constraint.value = false
1: constraint.final = false
5: response1 = 1
5: response2 = 1
5: constraint.value = false
5: constraint.final = false
6: response3 = 1
6: constraint.value = true
6: constraint.final = false
11: stimulus = 2
11: constraint.value = false
11: constraint.final = false
12: stimulus = 3
12: constraint.value = false
12: constraint.final = false
15: response1= 2
15: response2= 3
15: response3= 2
15: constraint.value = false
15: constraint.final = false
16: response1= 3
16: response2= 2
16: response3= 3
16: constraint.value = true
16: constraint.final = false
def SynchronizationTimingConstraintResponseSynchronization(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool):=
TADL2.fourValuedConjunction(TADL2.outputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
TADL2.pseudoInfty),
if (multipleOccurrences) then
{value = true, final: false}
else
TADL2.StrongSynchronizationConstraintReset(Map.keys(Map.remove(eventIndices, 0)), responseStreamCount,
tolerance, TADL2.pseudoInfty))SynchronizationTimingConstraintResponseSynchronizationReset(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool, resetTime: Int)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType responseSynchronization as defined in the Autosar Timing Extensions.
resets a negative output after resetTime
see SynchronizationTimingConstraintResponseSynchronization for more information.
def SynchronizationTimingConstraintResponseSynchronizationReset(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool, resetTime: Int):=
TADL2.fourValuedConjunction(TADL2.outputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
resetTime),
if (multipleOccurrences) then
{value = true, final: false}
else
TADL2.StrongSynchronizationConstraintReset(Map.keys(Map.remove(eventIndices, 0)), responseStreamCount,
tolerance, resetTime))SynchronizationTimingConstraintStimulusSynchronization(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType stimulusSynchronization as defined in the Autosar Timing Extensions.
The SynchronizationTimingConstraint on event chains for the synchronizationConstraintType stimulusSynchronization describes groups of streams, which stimulus events occur in common clusters. The parameter tolerance specifies the maximal length of these intervals. If the parameter multipleOccurrences is true, each of these streams must have at least one event in each of these intervals. If the parameter multipleOccurrences is false, each of these streams must have exactly one event in each of these intervals.
Usage Example
in response: Events[Int]
in stimulus1: Events[Int]
in stimulus2: Events[Int]
in stimulus3: Events[Int]
def tolerance = 2
def timeNow =
merge(time(stimulus1),
merge(time(stimulus2),
merge(time(stimulus3),
time(response))))
def eventStimulus:= if (defaultTime(response) >= timeNow) then Map.add(Map.empty[Int, Int], 0, default(response, -1)) else Map.empty[Int, Int]
def eventResponse1:= if (defaultTime(stimulus1) >= timeNow) then Map.add(eventStimulus, 1, default(stimulus1, -1)) else eventStimulus
def eventResponse2:= if (defaultTime(stimulus2) >= timeNow) then Map.add(eventResponse1, 2, default(stimulus2, -1)) else eventResponse1
def eventResponse3:= if (defaultTime(stimulus3) >= timeNow) then Map.add(eventResponse2, 3, default(stimulus3, -1)) else eventResponse2
def responseStreamCount = 3
def multipleOccurrences = false
def constraint= AUTOSAR_TIMEX.SynchronizationTimingConstraintStimulusSynchronization(eventResponse3, responseStreamCount, tolerance, multipleOccurrences)
out constraint.value
out constraint.final
Trace Example
option timeDomain:[-1,22]
1: stimulus1 = 1
1: constraint.value = true
1: constraint.final = false
5: stimulus1 = 1
5: stimulus2 = 1
5: stimulus3 = 1
5: constraint.value = true
5: constraint.final = false
6: response = 1
6: constraint.value = true
6: constraint.final = false
15: stimulus1 = 2
15: constraint.value = true
15: constraint.final = false
16: stimulus2 = 2
16: constraint.value = true
16: constraint.final = false
17: stimulus3 = 2
17: constraint.value = true
17: constraint.final = false
20: response = 2
20: constraint.value = true
20: constraint.final = false
def SynchronizationTimingConstraintStimulusSynchronization(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool):=
TADL2.fourValuedConjunction(TADL2.inputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
TADL2.pseudoInfty),
if (multipleOccurrences) then
{value = true, final: false}
else
TADL2.StrongSynchronizationConstraintReset(Map.keys(Map.remove(eventIndices, 0)), responseStreamCount,
tolerance, TADL2.pseudoInfty))SynchronizationTimingConstraintStimulusSynchronizationMultiple(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType stimulusSynchronization as defined in the Autosar Timing Extensions with parameter EventOccurrenceType = MultipleOccurrences
def SynchronizationTimingConstraintStimulusSynchronizationMultiple(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool):=
TADL2.inputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
TADL2.pseudoInfty)SynchronizationTimingConstraintStimulusSynchronizationReset(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool, resetTime: Int)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType stimulusSynchronization as defined in the Autosar Timing Extensions.
resets a negative output after resetTime
see SynchronizationTimingConstraintStimulusSynchronization for more information.
def SynchronizationTimingConstraintStimulusSynchronizationReset(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int, multipleOccurrences: Bool, resetTime: Int):=
TADL2.fourValuedConjunction(TADL2.inputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
resetTime),
if (multipleOccurrences) then
{value = true, final: false}
else
TADL2.StrongSynchronizationConstraintReset(Map.keys(Map.remove(eventIndices, 0)), responseStreamCount,
tolerance, resetTime))SynchronizationTimingConstraintStimulusSynchronizationSingle(eventIndices: Events[Map[Int, Int]], responseStreamCount: Int, tolerance: Int)
Checks the SynchronizationTimingConstraint on event chains and for the synchronizationConstraintType stimulusSynchronization as defined in the Autosar Timing Extensions with parameter EventOccurrenceType = SingleOccurrences
def SynchronizationTimingConstraintStimulusSynchronizationSingle(eventIndices: Events[Map[Int, Int]],
responseStreamCount: Int, tolerance: Int):=
TADL2.fourValuedConjunction(TADL2.inputSynchronizationConstraintReset(eventIndices, responseStreamCount, tolerance,
TADL2.pseudoInfty),
TADL2.StrongSynchronizationConstraintReset(Map.keys(Map.remove(eventIndices, 0)), responseStreamCount,
tolerance, TADL2.pseudoInfty))