TeSSLa Autosar Timex/TADL 2 extension

def ageConstraint(stimulus: Events[Int], response: Events[Int], minTimeDiff: Int, maxTimeDiff: Int):
			Events[fourValuedLogicValue] :=
    ageConstraintReset(stimulus, response, minTimeDiff, maxTimeDiff, pseudoInfty)

	def ageConstraintReset(stimulus: Events[Int], response: Events[Int], minTimeDiff: Int, maxTimeDiff: Int,
			resetTime: Int): Events[fourValuedLogicValue] := {
        #removes colors, that were before timeBound, from the list
        def removeOldStimulusColorsFromList(latestStimulusColors: List[Int],
                colorTimeStamps: Map[Int, Int], timeBound: Int): List[Int] :=
            # list empty
            if (List.size(latestStimulusColors) == 0) then
                latestStimulusColors
            else
                # oldest event not too old-> return current list
                if (Map.contains(colorTimeStamps, List.head(latestStimulusColors)) &&
                        Map.get(colorTimeStamps, List.head(latestStimulusColors)) >= timeBound) then
                    latestStimulusColors
                else
                    # recursive call without oldest color
                    removeOldStimulusColorsFromList(List.tail(latestStimulusColors), colorTimeStamps, timeBound)

        #removes colors, that were before timeBound, from the map
        def removeOldStimulusColorsFromSet(latestStimulusColors: List[Int],
                colorTimeStamps: Map[Int, Int], timeBound: Int): Map[Int, Int] :=
            if (List.size(latestStimulusColors) == 0) then
                colorTimeStamps
            else
                 # oldest event not too old-> return current map
                if (Map.contains(colorTimeStamps, List.head(latestStimulusColors)) &&
                        Map.get(colorTimeStamps, List.head(latestStimulusColors)) >= timeBound)  then
                    colorTimeStamps
                else
                    # recursive call without oldest color
                    removeOldStimulusColorsFromSet(List.tail(latestStimulusColors),
                        Map.remove(colorTimeStamps, List.head(latestStimulusColors)), timeBound)

        # map with unmatched stimulus events after stimulus
        def stimulusEventsNewStimulus : Events[Map[Int, Int]] :=
            # stimulus events in this timestamp-> insert event in Map, else keep previous map
            if (defaultTime(stimulus) >= defaultTime(response)) then
                Map.add(default(last(stimulusEvents, merge(stimulus, response)), Map.empty[Int, Int]),
                    stimulus, defaultTime(stimulus))
            else
                default(last(stimulusEvents, merge(stimulus, response)), Map.empty[Int, Int])
        #unmatched stimulus events, remove events that are too old
        def stimulusEvents:=
                slift3(default(last(stimulusColorsYoungerThanMax, stimulus), List.empty[Int]),
                    stimulusEventsNewStimulus,
                    defaultTime(merge(stimulus, response)) - maxTimeDiff,
                    removeOldStimulusColorsFromSet)

        #unmatched stimulus events, that are younger than maximum
        def stimulusColorsYoungerThanMax: Events[List[Int]]:=
            slift3(
                List.append(slift(default(last(stimulusColorsYoungerThanMax, stimulus), List.empty[Int]),
                        stimulus, List_remove), stimulus),
                stimulusEventsNewStimulus,
                defaultTime(merge(stimulus, response)) - maxTimeDiff,
                removeOldStimulusColorsFromList)

        #evaluation
        # 'now' has response event => time matches to unmatched stimulus event
        stillFulfillableReset(
            if ((!(defaultTime(stimulus) <= defaultTime(response))) ||
                    Map.contains(stimulusEventsNewStimulus, merge(response, -1)) &&
                    Map.get(stimulusEventsNewStimulus, merge(response, -1)) + minTimeDiff <= defaultTime(response) &&
                    Map.get(stimulusEventsNewStimulus, merge(response, -1)) + maxTimeDiff >= defaultTime(response)) then
                {value= true, final= false}
            else
                {value= false, final= true},
			resetTime)
    }

def arbitraryConstraint[A](e: Events[A], minDist: List[Int], maxDist: List[Int]): Events[fourValuedLogicValue] :=
    arbitraryConstraintRec(e, minDist, maxDist, 1, pseudoInfty)

	def arbitraryConstraintReset[A](e: Events[A], minDist: List[Int], maxDist: List[Int], resetTime: Int):
			Events[fourValuedLogicValue] :=
        arbitraryConstraintRec(e, minDist, maxDist, 1, resetTime)

def burstConstraint[A](e: Events[A], length: Int, maxOccurrences: Int, minDist: Int): Events[fourValuedLogicValue] :=
		burstConstraintReset(e, length, maxOccurrences, minDist, pseudoInfty)

	def burstConstraintReset[A](e: Events[A], length: Int, maxOccurrences: Int, minDist: Int,
			resetTime: Int): Events[fourValuedLogicValue] :=
        # application of repeatConstraint
		fourValuedConjunction(repeatConstraintReset(e, length, pseudoInfty, maxOccurrences, resetTime),
			repeatConstraintReset(e, minDist, pseudoInfty, 1, resetTime))

def checkEventChain(stimulus: Events[Int], response: Events[Int]): Events[fourValuedLogicValue]:=
		checkEventChainReset(stimulus, response, pseudoInfty)

	def checkEventChainReset(stimulus: Events[Int], response: Events[Int], resetTime: Int):
			Events[fourValuedLogicValue]:= {
		# next timestamp after 'falling flank'
		def failingTimeStamps: Events[Unit] =
			filter(mergeUnit(stimulus, response), last(result.final, mergeUnit(stimulus, response)) &&
					!(last(last(result.final, mergeUnit(stimulus, response)), mergeUnit(stimulus, response))))
		#timestamps, in which the state of the monitor is resetted
		def resets: Events[Unit]=
			delay(const(resetTime, failingTimeStamps)-(time(mergeUnit(stimulus, response)) -
					prev(time(mergeUnit(stimulus, response)))),
				failingTimeStamps)

		        # colors that occured in response-> not allows in stimulus anymore
        def previousResponseColors: Events[Set[Int]]:=
			merge(merge(const(Set.empty[Int], resets),
					Set.add(last(previousResponseColors, response), response)),
				Set.empty[Int])
        def result:= stillFulfillableReset(
            if on(merge(stimulus, response),
                # stimulus event-> color didn't occur in response earlier
                    if (defaultTime(stimulus) >= defaultTime(response)) then
                        !Set.contains(previousResponseColors, stimulus)
                    else
                        true) then
                {value= true, final= false}
            else
                {value= false, final= true},
			resetTime)
		result
	}

def delayConstraint[A, B](source: Events[A], target: Events[B], lower: Int, upper: Int) :
			Events[fourValuedLogicValue] :={
    delayConstraintReset(source, target, lower, upper, pseudoInfty)
}

def delayConstraintReset[A, B](source: Events[A], target: Events[B], lower: Int, upper: Int,
			resetTime: Int) : Events[fourValuedLogicValue] :={

    # timestamps of source events, which did not have matching target event yet,
    # including the timestamps, which matches in this this timestamp
    def unfinishedSourceTimesNewSource: Events[List[Int]] :=
        # 'now' has source event
        if (defaultTime(source) >= defaultTime(target)) then
            List.append(default(last(unfinishedSourceTimes, mergeUnit(source, target)), List.empty[Int]),
					time(source))
        else
            default(last(unfinishedSourceTimes, mergeUnit(source, target)), List.empty[Int])

    def unfinishedSourceTimesAfterReset: Events[List[Int]] :=
			if (List.size(unfinishedSourceTimesNewSource) != 0) then
				if (List.head(unfinishedSourceTimesNewSource) + resetTime < time(mergeUnit(source, target))) then
					removeItemsSmallerThanAFromListFront(unfinishedSourceTimesNewSource,
						time(mergeUnit(source, target)) - upper)
				else
					unfinishedSourceTimesNewSource
			else
				List.empty[Int]
    # timestamps of source events, which did not have matching target event yet
    def unfinishedSourceTimes: Events[List[Int]]:=
        # 'now' has target event
        if (defaultTime(source) <= defaultTime(target) &&
                # List has source event without matching target
                List.size(unfinishedSourceTimesAfterReset) > 0 &&
                # target event now matches with oldest source event
                List.head(unfinishedSourceTimesAfterReset) + lower <= defaultTime(target) &&
                List.head(unfinishedSourceTimesAfterReset) + upper >= defaultTime(target)) then
            #remove matched target events
            merge(slift(unfinishedSourceTimesAfterReset, defaultTime(target) - lower + 1,
                    removeItemsSmallerThanAFromListFront),
                List.empty[Int])
        else
            merge(unfinishedSourceTimesAfterReset, List.empty[Int])
    # timestamps, in which the evaluation occurs
    def evaluateTimes = mergeUnit(mergeUnit(source, target),
        safeDelay(if (List.size(unfinishedSourceTimes) == 0) then
                -1
            else
                List.head(unfinishedSourceTimes) + upper - time(mergeUnit(source, target))+1,
            mergeUnit(source, target)))

    stillFulfillableReset(
        # no unfinished source events -> current true
        if (List.size(unfinishedSourceTimes) == 0) then
            {value= true, final= false}
        else
            # oldest source event can still be finished-> current false
            if (time(evaluateTimes) <= List.head(unfinishedSourceTimes) + upper) then
                {value= false, final= false}
            # oldest source event is too old -> final false
            else
                {value= false, final= true},
        resetTime)
}

def executionTimeConstraint[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D],
        lower: Int, upper: Int): Events[fourValuedLogicValue] :={
    executionTimeConstraintReset(start, end, preempt, resume, lower, upper, pseudoInfty)
}

	def executionTimeConstraintReset[A, B, C, D](start: Events[A], end: Events[B], preempt: Events[C], resume: Events[D],
            lower: Int, upper: Int, resetTime: Int): Events[fourValuedLogicValue] :={
        # timestamps, when the constraint is evaluated
        def inputTimes: Events[Unit] := mergeUnit(mergeUnit(mergeUnit(start, end), preempt), resume)
        # timestamps, in which the evaluation occurs
        def evaluateTimes: Events[Unit] :=
            mergeUnit(inputTimes, safeDelay(if (time(inputTimes) != defaultTime(end) &&
                                                    time(inputTimes) != defaultTime(preempt)) then
                                                upper - execTime + 1
                                            else
                                                -1, inputTimes))

        # evaluation
        def execTime : Events[Int] := runtime(start, evaluateTimes) - resetSum(runtime(preempt, resume), start)
        # 'now' is end event

        stillFulfillableReset(
            #first event or correct distance to X
            if (if (time(evaluateTimes) == defaultTime(end)) then
                    lower <= execTime && execTime <= upper
                else
                    #ignore lower
                    execTime <= upper) then
                {value= true, final= false}
            else
                {value= false, final= true},
			resetTime)
    }

liftable def fourValuedConjunction(a: fourValuedLogicValue, b: fourValuedLogicValue):=
    if ((!a.value && a.final) || (!b.value && b.final)) then
        {value= false, final= true}
    else
        if ((!a.value && !a.final) || (!b.value && !b.final)) then
            {value= false, final= false}
        else
            if ((a.value && !a.final) || (b.value && !b.final)) then
                {value= true, final= false}
            else
                {value= true, final= true}

	def inputSynchronizationConstraint10(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
            stimulus8: Events[Int], stimulus9: Events[Int], stimulus10: Events[Int], response: Events[Int],
            tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset10(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, stimulus6,
			stimulus7, stimulus8, stimulus9, stimulus10, response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint2(stimulus1: Events[Int], stimulus2: Events[Int], response: Events[Int],
            tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset2(stimulus1, stimulus2, response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint3(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
			response: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset3(stimulus1, stimulus2, stimulus3, response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint4(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], response: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset4(stimulus1, stimulus2, stimulus3, stimulus4, response, tolerance,
			pseudoInfty)

def inputSynchronizationConstraint5(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], response: Events[Int], tolerance: Int):
			Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset5(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, response,
			tolerance, pseudoInfty)

	def inputSynchronizationConstraint6(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], response: Events[Int],
            tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset6(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, stimulus6,
			response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint7(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
            response: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset7(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, stimulus6,
			stimulus7, response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint8(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
            stimulus8: Events[Int], response: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset8(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, stimulus6,
			stimulus7, stimulus8, response, tolerance, pseudoInfty)

	def inputSynchronizationConstraint9(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
            stimulus8: Events[Int], stimulus9: Events[Int], response: Events[Int], tolerance: Int):
			Events[fourValuedLogicValue] :=
		inputSynchronizationConstraintReset9(stimulus1, stimulus2, stimulus3, stimulus4, stimulus5, stimulus6,
			stimulus7, stimulus8, stimulus9, response, tolerance, pseudoInfty)

def inputSynchronizationConstraintReset(eventStreamIndices: Events[Map[Int, Int]], stimulusStreamCount: Int,
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:= {
    # Help functions

    #builds the starting point for the state Map
    def buildEmptylatestEventTimes(stimulusStreamCount: Int): Map[Int, Map[Int, Int]] :=
        if (stimulusStreamCount == 0) then
            Map.empty[Int, Map[Int, Int]]
        else
            Map.add(buildEmptylatestEventTimes(stimulusStreamCount-1), stimulusStreamCount, Map.empty[Int, Int]);

    # adds stimulus events to stored events
    def addEventsToEmptylatestEventTimes(latestEventTimes: Map[Int, Map[Int, Int]], timeNow: Int,
            eventStreamIndices: Map[Int, Int]): Map[Int, Map[Int, Int]] :=
        addEventsToEmptylatestEventTimesRec(latestEventTimes, timeNow, eventStreamIndices, Map.keys(eventStreamIndices));

    def addEventsToEmptylatestEventTimesRec(latestEventTimes: Map[Int, Map[Int, Int]], timeNow: Int,
            eventStreamIndices: Map[Int, Int], remainingKeys: List[Int]): Map[Int, Map[Int, Int]] :=
        if (List.size(remainingKeys) == 0) then
            latestEventTimes
        else
            # if resoponse stream -> don't insert
            if (List.head(remainingKeys) == 0) then
                addEventsToEmptylatestEventTimesRec(latestEventTimes, timeNow, eventStreamIndices,
						List.tail(remainingKeys))
            else
                # insert head of map and recursive call
                addEventsToEmptylatestEventTimesRec(
                    Map.add(latestEventTimes, List.head(remainingKeys),
                        Map.add(Map.get(latestEventTimes, List.head(remainingKeys)), Map.get(eventStreamIndices,
								List.head(remainingKeys)), timeNow)),
                    timeNow, eventStreamIndices, List.tail(remainingKeys))
    # time of the oldest event of the given color
    def timeOldestEvent(latestEvents: Map[Int, Map[Int, Int]], color: Int, remainingKeys: List[Int]): Int :=
        #static if (Map.size(latestEvents) == 0 || List.size(remainingKeys) == 0) then
        if (List.size(remainingKeys) == 0) then
            pseudoInfty
        else
            if (Map.contains(Map.get(latestEvents, List.head(remainingKeys)), color)) then
                min(Map.get(Map.get(latestEvents, List.head(remainingKeys)), color),
                    timeOldestEvent(latestEvents, color, List.tail(remainingKeys)))
            else
                -pseudoInfty

    # time of the youngest event of the given color
    def timeYoungestEvent(latestEvents: Map[Int, Map[Int, Int]], color: Int, remainingKeys: List[Int]): Int :=
        #static if (Map.size(latestEvents) == 0 || List.size(remainingKeys) == 0) then
        if (List.size(remainingKeys) == 0) then
            -pseudoInfty
        else
            if (Map.contains(Map.get(latestEvents, List.head(remainingKeys)), color)) then
                max(Map.get(Map.get(latestEvents, List.head(remainingKeys)), color),
                    timeYoungestEvent(latestEvents, color, List.tail(remainingKeys)))
            else
                pseudoInfty

    # checks, if the synchronization cluster for the given color is fulfilled
    def clusterFulfilled(latestEventTimes: Map[Int, Map[Int, Int]], color: Int, tolerance: Int) : Bool =
        clusterFulfilledRec(latestEventTimes, Map.keys(latestEventTimes), color, tolerance)

    def clusterFulfilledRec(latestEventTimes: Map[Int, Map[Int, Int]], remainingKeys: List[Int], color: Int,
				tolerance: Int) : Bool =
        if (List.size(remainingKeys) == 0) then
            true
        else
            timeOldestEvent(latestEventTimes, color, remainingKeys) + tolerance >=
						timeYoungestEvent(latestEventTimes, color, remainingKeys) &&
            clusterFulfilledRec(latestEventTimes, List.tail(remainingKeys), color, tolerance)

    #stored information

    # time of last stimulus events with given color
    #   streamIndex -> (color -> time)
    def latestEventTimes: Events[Map[Int, Map[Int, Int]]] :=
        slift3(default(last(latestEventTimes, time(eventStreamIndices)), buildEmptylatestEventTimes(stimulusStreamCount)),
				time(eventStreamIndices), eventStreamIndices, addEventsToEmptylatestEventTimes)


    #evaluation
	   stillFulfillableReset(
        # response event-> valid cluster of the same color must exists
        if (Map.contains(eventStreamIndices, 0)) then
            if slift3(latestEventTimes, Map.get(eventStreamIndices, 0), tolerance, clusterFulfilled) then
                {value= true, final= false}
            else
                {value= false, final= true}
        else
            # no response event-> invalid trace
            {value= true, final= false},
			resetTime)

}

def inputSynchronizationConstraintReset10(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
        stimulus8: Events[Int], stimulus9: Events[Int], stimulus10: Events[Int], response: Events[Int],
        tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
        merge(time(stimulus5),
        merge(time(stimulus6),
        merge(time(stimulus7),
        merge(time(stimulus8),
        merge(time(stimulus9),
        merge(time(stimulus10),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
    def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4
    def eventResponse6:= if (defaultTime(stimulus6)  >= timeNow) then Map.add(eventResponse5, 6, default(stimulus6, -1)) else eventResponse5
    def eventResponse7:= if (defaultTime(stimulus7)  >= timeNow) then Map.add(eventResponse6, 7, default(stimulus7, -1)) else eventResponse6
    def eventResponse8:= if (defaultTime(stimulus8)  >= timeNow) then Map.add(eventResponse7, 8, default(stimulus8, -1)) else eventResponse7
    def eventResponse9:= if (defaultTime(stimulus9)  >= timeNow) then Map.add(eventResponse8, 9, default(stimulus9, -1)) else eventResponse8
    def eventResponse10:= if (defaultTime(stimulus10)  >= timeNow) then Map.add(eventResponse9, 10, default(stimulus10, -1)) else eventResponse9
    inputSynchronizationConstraintReset(eventResponse10, 10, tolerance, resetTime)
}

def inputSynchronizationConstraintReset2(stimulus1: Events[Int], stimulus2: Events[Int], response: Events[Int],
        tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
            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

    inputSynchronizationConstraintReset(eventResponse2, 2, tolerance, resetTime)
}

def inputSynchronizationConstraintReset3(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        response: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    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

    inputSynchronizationConstraintReset(eventResponse3, 3, tolerance, resetTime)
}

def inputSynchronizationConstraintReset4(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], response: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3

    inputSynchronizationConstraintReset(eventResponse4, 4, tolerance, resetTime)
}

	def inputSynchronizationConstraintReset5(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
            stimulus4: Events[Int], stimulus5: Events[Int], response: Events[Int], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue] :={
        def timeNow =
            merge(time(stimulus1),
            merge(time(stimulus2),
            merge(time(stimulus3),
            merge(time(stimulus4),
            merge(time(stimulus5),
                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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
        def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4

        inputSynchronizationConstraintReset(eventResponse5, 5, tolerance, resetTime)
    }

def inputSynchronizationConstraintReset6(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], response: Events[Int],
        tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
        merge(time(stimulus5),
        merge(time(stimulus6),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
    def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4
    def eventResponse6:= if (defaultTime(stimulus6)  >= timeNow) then Map.add(eventResponse5, 6, default(stimulus6, -1)) else eventResponse5

    inputSynchronizationConstraintReset(eventResponse6, 6, tolerance, resetTime)
}

def inputSynchronizationConstraintReset7(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
        response: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
        merge(time(stimulus5),
        merge(time(stimulus6),
        merge(time(stimulus7),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
    def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4
    def eventResponse6:= if (defaultTime(stimulus6)  >= timeNow) then Map.add(eventResponse5, 6, default(stimulus6, -1)) else eventResponse5
    def eventResponse7:= if (defaultTime(stimulus7)  >= timeNow) then Map.add(eventResponse6, 7, default(stimulus7, -1)) else eventResponse6

    inputSynchronizationConstraintReset(eventResponse7, 7, tolerance, resetTime)
}

def inputSynchronizationConstraintReset8(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
        stimulus8: Events[Int], response: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
        merge(time(stimulus5),
        merge(time(stimulus6),
        merge(time(stimulus7),
        merge(time(stimulus8),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
    def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4
    def eventResponse6:= if (defaultTime(stimulus6)  >= timeNow) then Map.add(eventResponse5, 6, default(stimulus6, -1)) else eventResponse5
    def eventResponse7:= if (defaultTime(stimulus7)  >= timeNow) then Map.add(eventResponse6, 7, default(stimulus7, -1)) else eventResponse6
    def eventResponse8:= if (defaultTime(stimulus8)  >= timeNow) then Map.add(eventResponse7, 8, default(stimulus8, -1)) else eventResponse7

    inputSynchronizationConstraintReset(eventResponse8, 8, tolerance, resetTime)
}

def inputSynchronizationConstraintReset9(stimulus1: Events[Int], stimulus2: Events[Int], stimulus3: Events[Int],
        stimulus4: Events[Int], stimulus5: Events[Int], stimulus6: Events[Int], stimulus7: Events[Int],
        stimulus8: Events[Int], stimulus9: Events[Int], response: Events[Int], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus1),
        merge(time(stimulus2),
        merge(time(stimulus3),
        merge(time(stimulus4),
        merge(time(stimulus5),
        merge(time(stimulus6),
        merge(time(stimulus7),
        merge(time(stimulus8),
        merge(time(stimulus9),
            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 eventResponse4:= if (defaultTime(stimulus4)  >= timeNow) then Map.add(eventResponse3, 4, default(stimulus4, -1)) else eventResponse3
    def eventResponse5:= if (defaultTime(stimulus5)  >= timeNow) then Map.add(eventResponse4, 5, default(stimulus5, -1)) else eventResponse4
    def eventResponse6:= if (defaultTime(stimulus6)  >= timeNow) then Map.add(eventResponse5, 6, default(stimulus6, -1)) else eventResponse5
    def eventResponse7:= if (defaultTime(stimulus7)  >= timeNow) then Map.add(eventResponse6, 7, default(stimulus7, -1)) else eventResponse6
    def eventResponse8:= if (defaultTime(stimulus8)  >= timeNow) then Map.add(eventResponse7, 8, default(stimulus8, -1)) else eventResponse7
    def eventResponse9:= if (defaultTime(stimulus9)  >= timeNow) then Map.add(eventResponse8, 9, default(stimulus9, -1)) else eventResponse8

    inputSynchronizationConstraintReset(eventResponse9, 9, tolerance, resetTime)
}

	def orderConstraint[A, B](source: Events[A], target: Events[B]): Events[fourValuedLogicValue] :=
		orderConstraintReset(source, target, pseudoInfty)

	def orderConstraintReset[A, B](source: Events[A], target: Events[B], resetTime: Int):
			Events[fourValuedLogicValue] := {
		# next timestamp after 'falling flank'
		def failingTimeStamps: Events[Unit] =
			filter(mergeUnit(source, target), last(result.final, mergeUnit(source, target)) &&
					!(last(last(result.final, mergeUnit(source, target)), mergeUnit(source, target))))
		#timestamps, in which the state of the monitor is resetted
		def resets: Events[Unit]=
			delay(const(resetTime, failingTimeStamps)-(time(mergeUnit(source, target)) -
					prev(time(mergeUnit(source, target)))),
				failingTimeStamps)

		#reset count for both streams
		def sourceCount: Events[Int] = resetCount2(source, resets)
		def targetCount: Events[Int] = resetCount2(target, resets)

        def result := stillFulfillableReset(
            #number of events on both streams equal-> currently true
            if sourceCount == targetCount then
                if (defaultTime(source) == defaultTime(target) && defaultTime(source) != -1) then
                    {value= false, final= true}
                else
                    {value= true, final= false}
            else
                # more source than target events-> currently false
                if (sourceCount >= targetCount) then
                    {value= false, final= false}
                else
                    # more target than source events-> false
                    {value= false, final= true},
			resetTime)
		#output
		result
	}

	def outputSynchronizationConstraint10(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
            response7: Events[Int], response8: Events[Int], response9: Events[Int], response10: Events[Int],
            tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset10(stimulus, response1, response2, response3, response4, response5,
			response6, response7, response8, response9, response10, tolerance, pseudoInfty)

	def outputSynchronizationConstraint2(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
			tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset2(stimulus, response1, response2, tolerance, pseudoInfty)

	def outputSynchronizationConstraint3(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset3(stimulus, response1, response2, response3, tolerance, pseudoInfty)

	def outputSynchronizationConstraint4(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset4(stimulus, response1, response2, response3, response4, tolerance,
			pseudoInfty)

	def outputSynchronizationConstraint5(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], tolerance: Int):
            Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset5(stimulus, response1, response2, response3, response4, response5,
			tolerance, pseudoInfty)

	def outputSynchronizationConstraint6(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
            tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset6(stimulus, response1, response2, response3, response4, response5,
			response6, tolerance, pseudoInfty)

	def outputSynchronizationConstraint7(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
            response7: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset7(stimulus, response1, response2, response3, response4, response5,
			response6, response7, tolerance, pseudoInfty)

	def outputSynchronizationConstraint8(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
            response7: Events[Int], response8: Events[Int], tolerance: Int): Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset8(stimulus, response1, response2, response3, response4, response5,
			response6, response7, response8, tolerance, pseudoInfty)

	def outputSynchronizationConstraint9(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
            response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
            response7: Events[Int], response8: Events[Int], response9: Events[Int], tolerance: Int):
			Events[fourValuedLogicValue] :=
		outputSynchronizationConstraintReset9(stimulus, response1, response2, response3, response4, response5,
			response6, response7, response8, response9, tolerance, pseudoInfty)

def outputSynchronizationConstraintReset(eventStreamIndices: Events[Map[Int, Int]],
			responseStreamCount: Int, tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:= {
    ##### Help funtions #####
    # add an empty cluster to storedClusters
    def addNewCluster(storedClusters: Map[Int, outputSynchronizationCluster], newColor: Int, time: Int,
				responseStreamCount: Int): Map[Int, outputSynchronizationCluster] :=
        Map.add(storedClusters, newColor, buildOutputSynchronizationCluster(time, responseStreamCount))

    #removes every entry of listToRemove from the given set
    liftable def removeListFromSet[A](aSet: Set[A], listToRemove: List[A]): Set[A]:=
        if (List.size(listToRemove) == 0) then
            aSet
        else
            removeListFromSet(
                if (Set.contains(aSet, List.head(listToRemove))) then
                    Set.remove(aSet, List.head(listToRemove))
                else
                    aSet,
                List.tail(listToRemove))

    # build list from aMap with all keys given in remainingKeys
    liftable def mapValuesToList[A, B](aMap: Map[A, B], remainingKeys: List[A]): List[B]:=
        if List.size(remainingKeys) == 0 then
            List.empty[B]
        else
            List.append(mapValuesToList(aMap, List.tail(remainingKeys)),
                Map.get(aMap, List.head(remainingKeys)))

    # removes map entries with key = 0
    liftable def removeStimulusEvents(events: Map[Int, Int]): Map[Int, Int] :=
        if (Map.contains(events, 0)) then
            Map.remove(events, 0)
        else
            events
    #updates the stored synchronization clusters by all events in this timestamp (update or creation of new cluster)
    def updateSynchronizationClusters(storedClusters: Map[Int, outputSynchronizationCluster], events: Map[Int, Int],
				eventKeys: List[Int], unmatchedStimulusColors: Set[Int], timeNow: Int):
				Map[Int, outputSynchronizationCluster] := {
        # set the given stream in cluster to true
        def setStreamInSynchronizationCluster(cluster: outputSynchronizationCluster, stream: Int):
					outputSynchronizationCluster = {
				startTime = cluster.startTime,
				fulfilledStreams = Map.add(cluster.fulfilledStreams, stream, true)
			}

        if List.size(eventKeys) == 0 then
            storedClusters
        else
            updateSynchronizationClusters(
                # set stream to fulfilled in Cluster
                if (Map.contains(storedClusters, Map.get(events, List.head(eventKeys))) ||
							Set.contains(unmatchedStimulusColors, Map.get(events, List.head(eventKeys)))) then
                    Map.add(storedClusters, Map.get(events, List.head(eventKeys)),
                        setStreamInSynchronizationCluster(
                            Map.get(
                                # add new cluster, if needed
                                if ((!Map.contains(storedClusters, Map.get(events, List.head(eventKeys)))) &&
											Set.contains(unmatchedStimulusColors, Map.get(events, List.head(eventKeys)))) then
                                    addNewCluster(storedClusters,
											Map.get(events, List.head(eventKeys)), timeNow, responseStreamCount)
                                else
                                    storedClusters,
                                Map.get(events, List.head(eventKeys))),
                            List.head(eventKeys)))
                    else
                        storedClusters,
                events, List.tail(eventKeys), unmatchedStimulusColors, timeNow)
        }

    # check, if all streams are fulfilled in this cluster. Ignores timing
    def clusterFulfilled(fulfilledStreams: Map[Int, Bool], keys: List[Int]): Bool :=
        if (List.size(keys) == 0) then
            true
        else
            if (Map.get(fulfilledStreams,  List.head(keys))) then
                clusterFulfilled(fulfilledStreams, List.tail(keys))
            else
                false

    # searches for all fulfilled clusters in Map and returns their colors in a list
    #   storedClusters: Map with stored clusters (color -> cluster)
    liftable def fulfilledClustersInMapRec(storedClusters: Map[Int, outputSynchronizationCluster], aList: List[Int],
				keys: List[Int]): List[Int] :=
        if (List.size(keys) == 0) then
            aList
        else
            fulfilledClustersInMapRec(storedClusters,
                if (clusterFulfilled(Map.get(storedClusters, List.head(keys)).fulfilledStreams,
							Map.keys(Map.get(storedClusters, List.head(keys)).fulfilledStreams))) then
                    List.append(aList, List.head(keys))
                else
                    aList, List.tail(keys))

    # searches for all fulfilled clusters in Map and returns their colors in a list
    #   storedClusters: Map with stored clusters (color -> cluster)
    liftable def fulfilledClustersInMap(storedClusters: Map[Int, outputSynchronizationCluster]): List[Int] :=
        fulfilledClustersInMapRec(storedClusters, List.empty[Int], Map.keys(storedClusters))

    #removes clusters from Map
    def removeClusters(storedClusters: Map[Int, outputSynchronizationCluster], colorsToRemove: List[Int]):
            Map[Int, outputSynchronizationCluster] :=
        if (List.size(colorsToRemove) == 0) then
            storedClusters
        else
            removeClusters(Map.remove(storedClusters, List.head(colorsToRemove)), List.tail(colorsToRemove))

    liftable def startTimeOldestCluster(storedClustersBeforeRemove: Map[Int, outputSynchronizationCluster],
            keys: List[Int]): Int :=
        if (List.size(keys) == 0) then
            pseudoInfty-tolerance
        else
            min(Map.get(storedClustersBeforeRemove, List.head(keys)).startTime,
                startTimeOldestCluster(storedClustersBeforeRemove, List.tail(keys)))

    # Stored Information #

    #stimulus colors without matching target event
    def unmatchedStimulusColors: Events[Set[Int]] :=
            removeListFromSet(
                if (Map.contains(eventStreamIndices, 0)) then
                    Set.add(default(last(unmatchedStimulusColors, eventStreamIndices), Set.empty[Int]),
							Map.get(eventStreamIndices, 0))
                else
                    default(last(unmatchedStimulusColors, eventStreamIndices), Set.empty[Int]),
                mapValuesToList(removeStimulusEvents(eventStreamIndices), Map.keys(removeStimulusEvents(eventStreamIndices))))

    # synchronization clusters with new stimulus events
    def storedClustersBeforeRemove : Events[Map[Int, outputSynchronizationCluster]] :=
        merge(slift5(last(storedClusters, time(eventStreamIndices)), removeStimulusEvents(eventStreamIndices),
				Map.keys(removeStimulusEvents(eventStreamIndices)), prev(unmatchedStimulusColors),
        time(eventStreamIndices), updateSynchronizationClusters),
        Map.empty[Int, outputSynchronizationCluster])

    # stored clusters after removing the clusters, which were fulfilled in this timestamp
    def storedClusters: Events[Map[Int, outputSynchronizationCluster]] :=
			merge(on(resets, Map.empty[Int, outputSynchronizationCluster]),
				merge(slift(storedClustersBeforeRemove, slift1(storedClustersBeforeRemove, fulfilledClustersInMap),
						removeClusters),
					Map.empty[Int, outputSynchronizationCluster]))


    # timestamps, in which the evaluation occurs
    def evalTimes = time(mergeUnit(eventStreamIndices,
        TADL2.safeDelay(slift(storedClusters,
				Map.keys(storedClusters), startTimeOldestCluster) + tolerance - time(eventStreamIndices) + 1,
				eventStreamIndices)))

		# next timestamp after 'falling flank'
		def failingTimeStamps: Events[Unit] =
			filter(const((), eventStreamIndices), last(result.final, eventStreamIndices) &&
					!(last(last(result.final, eventStreamIndices), eventStreamIndices)))
		#timestamps, in which the state of the monitor is resetted
		def resets: Events[Unit]=
			delay(if (const(resetTime, failingTimeStamps)-(time(eventStreamIndices) - prev(time(eventStreamIndices))) > 0) then
				const(resetTime, failingTimeStamps)-(time(eventStreamIndices) - prev(time(eventStreamIndices))) else 1,
				failingTimeStamps)

    #no unfinished synchronization clusters and no unmatched Stimulus colors
		def result:=
			TADL2.stillFulfillableReset(
				if (Set.size(unmatchedStimulusColors) == 0 && Map.size(storedClusters) == 0) then
					{value= true, final= false}
				else
					# unfulfilled stimulus colors exist, all clusters are still fulfillable-> current false
					if startTimeOldestCluster(storedClusters, Map.keys(storedClusters)) + tolerance > evalTimes then
						{value= false, final= false}
					else
						{value= false, final= true},
				resetTime)
		#output
		result

}

def outputSynchronizationConstraintReset10(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
        response7: Events[Int], response8: Events[Int], response9: Events[Int], response10: Events[Int],
        tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
        merge(time(response5),
        merge(time(response6),
        merge(time(response7),
        merge(time(response8),
        merge(time(response9),
            time(response10)))))))))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4
    def eventResponse6:=
			if (defaultTime(response6)  >= timeNow) then
				Map.add(eventResponse5, 6, default(response6, -1))
			else
				eventResponse5
    def eventResponse7:=
			if (defaultTime(response7)  >= timeNow) then
				Map.add(eventResponse6, 7, default(response7, -1))
			else
				eventResponse6
    def eventResponse8:=
			if (defaultTime(response8)  >= timeNow) then
				Map.add(eventResponse7, 8, default(response8, -1))
			else
				eventResponse7
    def eventResponse9:=
			if (defaultTime(response9)  >= timeNow) then
				Map.add(eventResponse8, 9, default(response9, -1))
			else
				eventResponse8
    def eventResponse10:=
			if (defaultTime(response10)  >= timeNow) then
				Map.add(eventResponse9, 10, default(response10, -1))
			else
				eventResponse9

    outputSynchronizationConstraintReset(eventResponse10, 10, tolerance, resetTime)
}

def outputSynchronizationConstraintReset2(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        (time(response2))))

    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
    outputSynchronizationConstraintReset(eventResponse2, 2, tolerance, resetTime)
}

def outputSynchronizationConstraintReset3(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    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
    outputSynchronizationConstraintReset(eventResponse3, 3, tolerance, resetTime)
}

def outputSynchronizationConstraintReset4(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
            time(response4)))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3

    outputSynchronizationConstraintReset(eventResponse4, 4, tolerance, resetTime)
}

def outputSynchronizationConstraintReset5(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], tolerance: Int, resetTime: Int):
        Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
            time(response5))))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4

    outputSynchronizationConstraintReset(eventResponse5, 5, tolerance, resetTime)
}

def outputSynchronizationConstraintReset6(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
        tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
        merge(time(response5),
            time(response6)))))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4
    def eventResponse6:=
			if (defaultTime(response6)  >= timeNow) then
				Map.add(eventResponse5, 6, default(response6, -1))
			else
				eventResponse5

    outputSynchronizationConstraintReset(eventResponse6, 6, tolerance, resetTime)
}

def outputSynchronizationConstraintReset7(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
        response7: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
        merge(time(response5),
        merge(time(response6),
            time(response7))))))))

   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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4
    def eventResponse6:=
			if (defaultTime(response6)  >= timeNow) then
				Map.add(eventResponse5, 6, default(response6, -1))
			else
				eventResponse5
    def eventResponse7:=
			if (defaultTime(response7)  >= timeNow) then
				Map.add(eventResponse6, 7, default(response7, -1))
			else
				eventResponse6

    outputSynchronizationConstraintReset(eventResponse7, 7, tolerance, resetTime)
}

def outputSynchronizationConstraintReset8(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
        response7: Events[Int], response8: Events[Int], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
        merge(time(response5),
        merge(time(response6),
        merge(time(response7),
            time(response8)))))))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4
    def eventResponse6:=
			if (defaultTime(response6)  >= timeNow) then
				Map.add(eventResponse5, 6, default(response6, -1))
			else
				eventResponse5
    def eventResponse7:=
			if (defaultTime(response7)  >= timeNow) then
				Map.add(eventResponse6, 7, default(response7, -1))
			else
				eventResponse6
    def eventResponse8:=
			if (defaultTime(response8)  >= timeNow) then
				Map.add(eventResponse7, 8, default(response8, -1))
			else
				eventResponse7

    outputSynchronizationConstraintReset(eventResponse8, 8, tolerance, resetTime)
}

def outputSynchronizationConstraintReset9(stimulus: Events[Int], response1: Events[Int], response2: Events[Int],
        response3: Events[Int], response4: Events[Int], response5: Events[Int], response6: Events[Int],
        response7: Events[Int], response8: Events[Int], response9: Events[Int], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue] := {
    def timeNow =
        merge(time(stimulus),
        merge(time(response1),
        merge(time(response2),
        merge(time(response3),
        merge(time(response4),
        merge(time(response5),
        merge(time(response6),
        merge(time(response7),
        merge(time(response8),
            time(response9))))))))))

    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 eventResponse4:=
			if (defaultTime(response4)  >= timeNow) then
				Map.add(eventResponse3, 4, default(response4, -1))
			else
				eventResponse3
    def eventResponse5:=
			if (defaultTime(response5)  >= timeNow) then
				Map.add(eventResponse4, 5, default(response5, -1))
			else
				eventResponse4
    def eventResponse6:=
			if (defaultTime(response6)  >= timeNow) then
				Map.add(eventResponse5, 6, default(response6, -1))
			else
				eventResponse5
    def eventResponse7:=
			if (defaultTime(response7)  >= timeNow) then
				Map.add(eventResponse6, 7, default(response7, -1))
			else
				eventResponse6
    def eventResponse8:=
			if (defaultTime(response8)  >= timeNow) then
				Map.add(eventResponse7, 8, default(response8, -1))
			else
				eventResponse7
    def eventResponse9:=
			if (defaultTime(response9)  >= timeNow) then
				Map.add(eventResponse8, 9, default(response9, -1))
			else
				eventResponse8

    outputSynchronizationConstraintReset(eventResponse9, 9, tolerance, resetTime)
}

def patternConstraint[A](e: Events[A], periodX: Int, offset: Map[Int, Int], jitter: Int, minDist: Int) :
			Events[fourValuedLogicValue] :=
    patternConstraintReset(e, periodX, offset, jitter, minDist, pseudoInfty)

	def patternConstraintReset[A](e: Events[A], periodX: Int, offset: Map[Int, Int], jitter: Int,
			minDist: Int, resetTime: Int) : Events[fourValuedLogicValue] := {
	   liftable def aModuloBOr1if1(a: Int, b: Int): Int:=
            if b == 1 then 1 else a % b;
        # lower bound for latest x
        def lowerBoundX: Events[Int] :=
			if (last(res, e).final) then
				on(e, 0)
			else
				merge (
					# increase by period and adjust by offset and jitter
					if (aModuloBOr1if1(resetCount2(e, filter(e, last(res, e).final)), Map.size(offset))== 1 && !isFirst(e)) then
						max(last(lowerBoundX, e) + periodX,
							time(e) - Map.get(offset,
											(resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset))-jitter)
					#adjust by offset and jitter
					else
						max(last(lowerBoundX, e),
							time(e) - Map.get(offset,
										(resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset))-jitter),
					time(e) - Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset)) - jitter)
        # lower bound for latest x
        def upperBoundX: Events[Int] :=
			if (last(res, e).final) then
				on(e, pseudoInfty)
			else
				merge (
					# increase by period and adjust by offset and jitter
					if (aModuloBOr1if1(resetCount2(e, filter(e, last(res, e).final)), Map.size(offset))== 1 && !isFirst(e))  then
						min(last(upperBoundX, e) + periodX,
							time(e) - Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset)))
					else
					# adjust by offset and jitter
						min(last(upperBoundX, e),
							time(e) - Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset))),
					time(e) - Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset)))
        # timestamps, in which the evaluation occurs
        def evaluateTimes=
			mergeUnit(e,
				TADL2.safeDelay(upperBoundX + (if resetCount2(e, filter(e, last(res, e).final)) % Map.size(offset) == 0 then
													periodX
												else
													0) +
					Map.get(offset, resetCount2(e, filter(e, last(res, e).final)) % Map.size(offset)) + jitter - time(e) + 1, e))
        #evaluation
		def res: Events[fourValuedLogicValue]= TADL2.stillFulfillableReset(default(TADL2.fourValuedConjunction(
				# distance to x is correct-> current true, false otherwise
				if (lowerBoundX +
						Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset)) <=
					time(evaluateTimes) &&
						time(evaluateTimes) <= upperBoundX +
						Map.get(offset, (resetCount2(e, filter(e, last(res, e).final))-1) % Map.size(offset)) + jitter) then
					{value= true, final= false}
				else
					{value= false, final= true},
				TADL2.repeatConstraintReset(e, minDist, pseudoInfty, 1, resetTime)),
			{final= false, value = true}), resetTime)
		res
   }

def periodicConstraint[A](events: Events[A], period: Int, jitter: Int, minDist: Int) :=
    sporadicConstraint(events, period, period, jitter, minDist)

	def periodicConstraintReset[A](events: Events[A], period: Int, jitter: Int, minDist: Int, resetTime: Int) :=
        sporadicConstraintReset(events, period, period, jitter, minDist, resetTime)

def reactionConstraint(stimulus: Events[Int], response: Events[Int], minTimeDiff: Int, maxTimeDiff: Int):
			Events[fourValuedLogicValue] :=
    reactionConstraintReset(stimulus, response, minTimeDiff, maxTimeDiff, pseudoInfty)

	def reactionConstraintReset(stimulus: Events[Int], response: Events[Int], minTimeDiff: Int,
			maxTimeDiff: Int, resetTime: Int): Events[fourValuedLogicValue] := {
        # Map with unmatched stimulus events after stimulus (color->timestamp)
        def unmatchedStimulusEventsNewStimulus : Events[Map[Int, Int]]:= merge(
            if defaultTime(stimulus) >= defaultTime(response) &&
                    !Map.contains(last(unmatchedStimulusEvents, merge(stimulus, response)), stimulus) then
                Map.add(last(unmatchedStimulusEvents, merge(stimulus, response)), stimulus, defaultTime(stimulus))
            else
                last(unmatchedStimulusEvents, merge(stimulus, response)),
            Map.empty[Int, Int])
        def unmatchedStimulusEventsRemoveReset: Events[Map[Int, Int]]:=
			default(
				removeEventsAfterReset(unmatchedStimulusEventsNewStimulus,
					Map.keys(unmatchedStimulusEventsNewStimulus),
					time(mergeUnit(stimulus, response)),
					resetTime),
				Map.empty[Int, Int])
        # Map with unmatched stimulus events after response
        def unmatchedStimulusEvents := merge (
            if (defaultTime(stimulus) <= defaultTime(response) &&
                    Map.contains(unmatchedStimulusEventsRemoveReset, merge(response, -1)) &&
                    Map.get(unmatchedStimulusEventsRemoveReset, merge(response, -1)) + minTimeDiff <=
						defaultTime(response) &&
                    Map.get(unmatchedStimulusEventsRemoveReset, merge(response, -1)) + maxTimeDiff >=
						defaultTime(response)) then
                Map.remove(unmatchedStimulusEventsRemoveReset, response)
            else
                unmatchedStimulusEventsRemoveReset,
            unmatchedStimulusEventsRemoveReset)
        # timestamps, in which the evaluation occurs
        def evaluateTimes = mergeUnit(mergeUnit(stimulus, response),
                safeDelay(slift1(unmatchedStimulusEvents, mapMinimumValue) + maxTimeDiff -
                    time(mergeUnit(stimulus, response)) + 1,
                    mergeUnit(stimulus, response)))

        #evaluation
        # no unmatched stimulus events-> currently true
        stillFulfillableReset(if (Map.size(unmatchedStimulusEvents) == 0) then
            {value= true, final= false}
        else
            # all unmatched stimulus events can still be matched-> currently false
            if (slift1(unmatchedStimulusEvents, mapMinimumValue) + maxTimeDiff >= time(evaluateTimes)) then
                {value= false, final= false}
            else
                {value= false, final= true}, resetTime)
	}

def repeatConstraint[A](e: Events[A], lower: Int, upper: Int, span: Int): Events[fourValuedLogicValue] :=
		repeatConstraintReset(e, lower, upper, span, pseudoInfty)

	def repeatConstraintReset[A](e: Events[A], lower: Int, upper: Int, span: Int, resetTime: Int):
		Events[fourValuedLogicValue] := {
        #stored state
        def latestSpanEventTimes: Events[List[Int]]:=
            if TADL2.defaultTime(e) == 0 then
                List.append(List.empty[Int], TADL2.defaultTime(e))
            else
                default(
                    List.append(
                        if (List.size(last(latestSpanEventTimes, e)) > span) then
                            List.tail(last(latestSpanEventTimes, TADL2.defaultTime(e)))
                        else
                            last(latestSpanEventTimes, e),
                        TADL2.defaultTime(e)),
                    List.empty[Int])

        # timestamps, in which the evaluation occurs
        def delayPeriod :=
			if (upper == pseudoInfty || upper < 0) then
				-1
			else
				if (defaultTime(e) == defaultTime(firstEvent(e))) then
					List.head(latestSpanEventTimes) + upper - time(e) + 1
				else
					List.head(List.tail(latestSpanEventTimes)) + upper - time(e) + 1

        def evaluateTimes :=
            mergeUnit(e, safeDelay(delayPeriod, e))

        stillFulfillableReset(
            # more than span events occured-> distance to span-1^th event is relevant
            if (List.size(latestSpanEventTimes) > span) then
                if List.head(latestSpanEventTimes) + lower <= time(evaluateTimes) &&
                        (upper == pseudoInfty || List.head(latestSpanEventTimes) + upper >= time(evaluateTimes)) then
                    {value= true, final= false}
                else
                    {value= false, final= true}
            else
                # less than span events occurred-> first event must be younger than upper
                if (upper == pseudoInfty || List.head(latestSpanEventTimes) + upper >= time(evaluateTimes)) then
                    {value= true, final= false}
                else
                    {value= false, final= true},
			resetTime)

    }

	def repetitionConstraint[A](e: Events[A], lower: Int, upper: Int, span: Int, jitter: Int):
			Events[fourValuedLogicValue] := {
		repetitionConstraintReset(e, lower, upper, span, jitter, pseudoInfty)
	}

	def repetitionConstraintReset[A](events: Events[A], lower: Int, upper: Int, span: Int, jitter: Int,
			resetTime: Int): Events[fourValuedLogicValue] := {
        # lower bound for current x
        def lowerBoundXNow: Events[Int] =
            if (List.size(last(LowerBoundX, events)) < span) then
                time(events)-jitter
            else
                max(List.head(last(LowerBoundX, events)), time(events)-jitter)
        # upper bound for current x
        def upperBoundXNow: Events[Int] =
            if (List.size(last(UpperBoundX, events)) < span) then
                time(events)
            else
                min(List.head(last(UpperBoundX, events)), time(events))

        # lower bound for span next x
        def LowerBoundX: Events[List[Int]]:= merge(
			if (last(res, events).final) then
				List.empty[Int]
			else
				if (List.size(last(LowerBoundX, events)) < span) then
				   List.append(last(LowerBoundX, events), lowerBoundXNow + lower)
				else
					List.append(last(List.tail(LowerBoundX), events), lowerBoundXNow + lower),
            List.empty[Int]
        )

         # upper bound for span next x
        def UpperBoundX: Events[List[Int]]:= merge(
			if (last(res, events).final) then
				List.empty[Int]
			else
				if (List.size(last(UpperBoundX, events)) < span) then
					List.append(last(UpperBoundX, events), upperBoundXNow+upper)
				else
					List.append(last(List.tail(UpperBoundX), events), upperBoundXNow + upper),
            List.empty[Int]
        )
        # timestamps, in which the evaluation occurs
        def evaluateTimes = mergeUnit(events,
            TADL2.safeDelay((if (List.size(UpperBoundX) == 0) then 0 else List.head(UpperBoundX)) +
                    jitter - time(events)+1, events))
        # Evaluation
        def res:= TADL2.stillFulfillableReset(
            #first event or correct distance to X
            if (List.size(LowerBoundX) == 0 && List.size(UpperBoundX) == 0) ||
                    lowerBoundXNow <= time(evaluateTimes) &&
                    upperBoundXNow + jitter >= time(evaluateTimes) then
                {value= true, final= false}
            else
                {value= false, final= true},
			resetTime)
		res
    }

	def resetCount2[A, B](events: Events[A], reset: Events[B]): Events[Int] = {
		def minusStream: Events[Int]=
			merge(
				if default((time(reset) >= time(events)), false) then
					if default((time(reset) == time(events)), false) then
						count(events)-1
					else
						count(events)
				else
					last(minusStream, mergeUnit(events, reset)),
				0)
		count(events) - minusStream
	}

def sporadicConstraint[A](e: Events[A], lower: Int, upper: Int, jitter: Int, minDist: Int):
			Events[fourValuedLogicValue]:=
    # application of repeat and repetititonConstraint
		fourValuedConjunction(repetitionConstraint(e, lower, upper, 1, jitter),
			repeatConstraint(e, minDist, pseudoInfty, 1))

	def sporadicConstraintReset[A](e: Events[A], lower: Int, upper: Int, jitter: Int, minDist: Int,
			ResetTime: Int): Events[fourValuedLogicValue]:=
        # application of repeat and repetititonConstraint
		fourValuedConjunction(repetitionConstraintReset(e, lower, upper, 1, jitter, ResetTime),
			repeatConstraintReset(e, minDist, pseudoInfty, 1, ResetTime))

def stillFulfillable(events: Events[fourValuedLogicValue]): Events[fourValuedLogicValue] :={
    def storage: Events[Bool] :=
        default(last(storage, events), true) && events != {value= false, final= true}

    if storage then
        events
    else
        {value= false, final= true}
}

	def stillFulfillableReset(events: Events[fourValuedLogicValue], resetTime: Int): Events[fourValuedLogicValue] :={
		# is the value currently final false?
		def isFinalFalse: Events[Bool] =
			default(last(isFinalFalseReset, events) || (events.final == true && events.value == false), false)
		# since which timestamp is the value final false?
		def finalFalseSince: Events[Int] =
			default(
				if (events.final && !events.value) && !prev(isFinalFalse) then
					time(events)
				else
					last(finalFalseSince, isFinalFalse),
				pseudoInfty)
		def isFinalFalseReset: Events[Bool] =
			merge(
				if (finalFalseSince + resetTime < time (events)) then
					false
				else
					isFinalFalse,
			isFinalFalse)
		#output
		if (isFinalFalseReset) then
			{value= false, final= true}
		else
			events
	}

	def strongDelayConstraint[A, B](source: Events[A], target: Events[B], lower: Int, upper: Int) :=
		strongDelayConstraintReset(source, target, lower, upper, pseudoInfty)

def strongDelayConstraintReset[A, B](source: Events[A], target: Events[B], lower: Int, upper: Int,
			resetTime: Int) :={
    # timestamps of source events, which did not have matching target event yet,
    # including the timestamps, which matches in this this timestamp
    def unfinishedSourceTimesNewSource:=
        #current timeStamp has source event
        if (TADL2.defaultTime(source) >= TADL2.defaultTime(target)) then
            # append timestamp to list
            List.append(default(last(unfinishedSourceTimes, mergeUnit(source, target)), List.empty[Int]),
					time(source))
        else
            default(last(unfinishedSourceTimes, mergeUnit(source, target)), List.empty[Int])
		# remove events that are older than resetTime
		def unfinishedSourceTimesAfterReset:=
			if List.size(unfinishedSourceTimesNewSource) != 0 then
				if (List.head(unfinishedSourceTimesNewSource) + resetTime < time(mergeUnit(source, target))) then
					TADL2.removeItemsSmallerThanAFromListFront(unfinishedSourceTimesNewSource,
						time(mergeUnit(source, target)) - upper)
				else
					unfinishedSourceTimesNewSource
			else
				List.empty[Int]
    # timestamps of source events, which did not have matching target event yet
    def unfinishedSourceTimes: Events[List[Int]]:=
        #current timeStamp has target event
        if (defaultTime(source) <= defaultTime(target)) then
            # removing possible-> remove
            if List.size(unfinishedSourceTimesAfterReset) != 0 then
                # if matching time distance to oldest stored event
                if (List.head(unfinishedSourceTimesAfterReset) + lower <= defaultTime(target) &&
                        List.head(unfinishedSourceTimesAfterReset) + upper >= defaultTime(target)) then
                    # just keep tail
                    List.tail(unfinishedSourceTimesAfterReset)
                else
                    # return unchanged
                    unfinishedSourceTimesAfterReset
            else
                # removing not possible-> insert event, that triggers {value= false, final= true}
                List.append(List.empty[Int], -pseudoInfty)
        else
            unfinishedSourceTimesAfterReset

    # timestamps, in which the evaluation occurs
    def evaluateTimes = mergeUnit(mergeUnit(source, target),
        safeDelay(if (List.size(unfinishedSourceTimes) == 0) then
                -1
            else
                List.head(unfinishedSourceTimes) + upper - time(mergeUnit(source, target))+1,
            mergeUnit(source, target)))

    # output
    stillFulfillableReset(
        # no unmatched source event-> current true
        if (List.size(unfinishedSourceTimes) == 0) then
            {value= true, final= false}
        else
            # target event, but no stored source event-> false
            if (List.size(unfinishedSourceTimesAfterReset) == 0) then
                {value= false, final= true}
            else
            #    # current timestamp has target event
                if (TADL2.defaultTime(target) >= time(evaluateTimes)) then
                    # correct distance-> current false
                    if (List.head(unfinishedSourceTimesAfterReset) + lower <= TADL2.defaultTime(target) &&
                            List.head(unfinishedSourceTimesAfterReset) + upper >= TADL2.defaultTime(target)) then
                        {value= false, final= false}
                    else
                        {value= false, final= true}
                else
                    # distance must only be smaller than upper
                    if List.head(unfinishedSourceTimesAfterReset) + upper >= TADL2.defaultTime(evaluateTimes) then
                        {value= false, final= false}
                    else
                        {value= false, final= true},
			resetTime)

}

def StrongSynchronizationConstraint10[A, B, C, D, E, F, G, H, I, J](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], events10: Events[J], tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset10(events1, events2, events3, events4, events5, events6, events7,
			events8, events9, events10, tolerance, pseudoInfty)

def StrongSynchronizationConstraint2[A, B](events1: Events[A], events2: Events[B], tolerance: Int):
        Events[fourValuedLogicValue]:=
    StrongSynchronizationConstraintReset2(events1, events2, tolerance, pseudoInfty)

def StrongSynchronizationConstraint3[A, B, C](events1: Events[A], events2: Events[B], events3: Events[C],
			tolerance: Int): Events[fourValuedLogicValue]:=
    StrongSynchronizationConstraintReset3(events1, events2, events3, tolerance, pseudoInfty)

def StrongSynchronizationConstraint4[A, B, C, D](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset4(events1, events2, events3, events4, tolerance, pseudoInfty)

def StrongSynchronizationConstraint5[A, B, C, D, E](events1: Events[A], events2: Events[B], events3: Events[C],
        events4: Events[D], events5: Events[E], tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset5(events1, events2, events3, events4, events5, tolerance,
			pseudoInfty)

def StrongSynchronizationConstraint6[A, B, C, D, E, F](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], tolerance: Int):
			Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset6(events1, events2, events3, events4, events5, events6, tolerance,
			pseudoInfty)

def StrongSynchronizationConstraint7[A, B, C, D, E, F, G](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset7(events1, events2, events3, events4, events5, events6, events7,
			tolerance, pseudoInfty)

def StrongSynchronizationConstraint8[A, B, C, D, E, F, G, H](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset8(events1, events2, events3, events4, events5, events6, events7,
			events8, tolerance, pseudoInfty)

def StrongSynchronizationConstraint9[A, B, C, D, E, F, G, H, I](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], tolerance: Int): Events[fourValuedLogicValue]:=
		StrongSynchronizationConstraintReset9(events1, events2, events3, events4, events5, events6, events7,
			events8, events9, tolerance, pseudoInfty)

	def StrongSynchronizationConstraintReset(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int,
		resetTime: Int): Events[fourValuedLogicValue]:= {

        # inserts one events to the active clusters. Creates new cluster, if needed.
        # insertes only, if cluster not too old
        # runtime: list.length(activeClusters)
        liftable def insertEvent(activeClusters: List[synchronizationCluster], eventIndex: Int, timeNow: Int):
				List[synchronizationCluster] :=
            # no more clusters to check -> create new cluster
            if (List.size(activeClusters) == 0) then
                List.append(activeClusters, {startTime= timeNow,
                    fulfilledStreams= Map.add(TADL2.buildMap(streamCount, false), eventIndex, true)})
            else
                # stream index already was in head cluster or too old-> check next one
                if (Map.get(List.head(activeClusters).fulfilledStreams, eventIndex) ||
                        List.head(activeClusters).startTime + tolerance < timeNow) then
                    List.prepend(List.head(activeClusters), insertEvent(List.tail(activeClusters), eventIndex, timeNow))
                #found matching cluster-> set stream in this cluster to true
                else
                    List.prepend({startTime= List.head(activeClusters).startTime,
                                fulfilledStreams= Map.add(List.head(activeClusters).fulfilledStreams, eventIndex, true)},
                        List.tail(activeClusters))

        # inserts all events from eventIndices to the active clusters.
        # runtime: List.length(eventIndices) * list.length(activeClusters)
        liftable def insertEventsList(activeClusters: List[synchronizationCluster], eventIndices: List[Int],
				timeNow: Int): List[synchronizationCluster] :=
            if (List.size(eventIndices) == 0) then
                activeClusters
            else
                insertEventsList(insertEvent(activeClusters, List.head(eventIndices), timeNow),
                    List.tail(eventIndices), timeNow)

        # runtime: min(tolerance, List.length(eventIndices) * list.length(activeClusters))
        liftable def removeFulfilledClusters(activeClusters: List[synchronizationCluster]):
				List[synchronizationCluster]:=
            #head of list is fulfilled-> remove and check next list entry
            if (List.size(activeClusters) != 0 && TADL2.mapAllTrue(List.head(activeClusters).fulfilledStreams)) then
                removeFulfilledClusters(List.tail(activeClusters))
            # head of list is unfulfilled-> don't remove, rest can't be fulfilled either
            else
                activeClusters

		# delete clusters which were created before lastestAllowedTime
		liftable def removeOldClusters(activeClusters: List[synchronizationCluster], latestAllowedTime: Int):
				List[synchronizationCluster] =
			if (List.size(activeClusters) == 0) then
				activeClusters
			else
				if (List.head(activeClusters).startTime < latestAllowedTime) then
					removeOldClusters(List.tail(activeClusters), latestAllowedTime)
				else
					List.prepend(List.head(activeClusters),
						removeOldClusters(List.tail(activeClusters), latestAllowedTime))

        #state
		def activeClustersResetted: Events[List[synchronizationCluster]]:=
			merge(merge(on(resets, removeOldClusters(last(activeClustersState, resets), time(resets) - tolerance)),
					last(activeClustersState, mergeUnit(resets, eventIndices))),
				List.empty[synchronizationCluster])


        # list of active clusters
        def activeClustersState: Events[List[synchronizationCluster]]:=
				merge(removeFulfilledClusters(
					if (TADL2.defaultTime(resets) > TADL2.defaultTime(eventIndices) && TADL2.defaultTime(resets) != -1) then
						activeClustersResetted
					else
						insertEventsList(activeClustersResetted, eventIndices, time(eventIndices))),
				List.empty[synchronizationCluster])

        #delay
        def evalTimes:=
            time(mergeUnit(eventIndices,
                TADL2.safeDelay(if (List.size(activeClustersState) != 0) then
                         List.head(activeClustersState).startTime+ tolerance - time(eventIndices)+1
                     else
                        -1, eventIndices)))

		# next timestamp after 'falling flank'
		def failingTimeStamps: Events[Unit] =
			filter(const((), eventIndices), last(result.final, eventIndices) &&
					!(last(last(result.final, eventIndices), eventIndices)))
		#timestamps, in which the state of the monitor is resetted
		def resets: Events[Unit]=
			delay(if (const(resetTime, failingTimeStamps)-(time(eventIndices) - prev(time(eventIndices))) > 0) then
				const(resetTime, failingTimeStamps)-(time(eventIndices) - prev(time(eventIndices))) else 1,
				failingTimeStamps)

        #no unfulfilled clusters-> currently true
        def result:= TADL2.stillFulfillableReset(
			if List.size(activeClustersState) == 0 then
				{value= true, final= false}
			else
				# unfulfilled clusters exists, but not too old-> current false
				if (List.head(activeClustersState).startTime + tolerance > evalTimes) then
					{value= false, final= false}
				else
					# unfulfilled clusters are too old-> def. false
					{value= false, final= true},
			resetTime)

		#output
		result
    }

	def StrongSynchronizationConstraintReset10[A, B, C, D, E, F, G, H, I, J](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], events10: Events[J], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            mergeUnit(events1, events2), events3), events4), events5), events6), events7), events8), events9), events10))

        def eventList10:=
            if (defaultTime(events10) >= timeNow) then
                List.prepend(10, List.empty[Int])
            else
                List.empty[Int]

        def eventList9:=
            if (defaultTime(events9) >= timeNow) then
                List.prepend(9, eventList10)
            else
                eventList10

        def eventList8:=
            if (defaultTime(events8) >= timeNow) then
                List.prepend(8, eventList9)
            else
                eventList9

        def eventList7:=
            if (defaultTime(events7) >= timeNow) then
                List.prepend(7, eventList8)
            else
                eventList8

        def eventList6:=
            if (defaultTime(events6) >= timeNow) then
                List.prepend(6, eventList7)
            else
                eventList7

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, eventList6)
            else
                eventList6

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 10, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset2[A, B](events1: Events[A], events2: Events[B],
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(events1, events2))


        def eventList2:=
            if (defaultTime(events2) >= timeNow) then
                List.prepend(2, List.empty[Int])
            else
                List.empty[Int]

        def eventList:=
            if (defaultTime(events1) >= timeNow) then
                List.prepend(1, eventList2)
            else
                eventList2

        StrongSynchronizationConstraintReset(eventList, 2, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset3[A, B, C](events1: Events[A], events2: Events[B], events3: Events[C],
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
        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

        StrongSynchronizationConstraintReset(eventList, 3, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset4[A, B, C, D](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(events1, events2), events3), events4))

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, List.empty[Int])
            else
                List.empty[Int]

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 4, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset5[A, B, C, D, E](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            events1, events2), events3), events4), events5))

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, List.empty[Int])
            else
                List.empty[Int]

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 5, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset6[A, B, C, D, E, F](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], tolerance: Int,
			resetTime: Int): Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            events1, events2), events3), events4), events5), events6))

        def eventList6:=
            if (defaultTime(events6) >= timeNow) then
                List.prepend(6, List.empty[Int])
            else
                List.empty[Int]

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, eventList6)
            else
                eventList6

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 6, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset7[A, B, C, D, E, F, G](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            events1, events2), events3), events4), events5), events6), events7))

        def eventList7:=
            if (defaultTime(events7) >= timeNow) then
                List.prepend(7, List.empty[Int])
            else
                List.empty[Int]

        def eventList6:=
            if (defaultTime(events6) >= timeNow) then
                List.prepend(6, eventList7)
            else
                eventList7

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, eventList6)
            else
                eventList6

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 7, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset8[A, B, C, D, E, F, G, H](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            events1, events2), events3), events4), events5), events6), events7), events8))

        def eventList8:=
            if (defaultTime(events8) >= timeNow) then
                List.prepend(8, List.empty[Int])
            else
                List.empty[Int]

        def eventList7:=
            if (defaultTime(events7) >= timeNow) then
                List.prepend(7, eventList8)
            else
                eventList8

        def eventList6:=
            if (defaultTime(events6) >= timeNow) then
                List.prepend(6, eventList7)
            else
                eventList7

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, eventList6)
            else
                eventList6

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 8, tolerance, resetTime)
    }

	def StrongSynchronizationConstraintReset9[A, B, C, D, E, F, G, H, I](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue]:={
        def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
            events1, events2), events3), events4), events5), events6), events7), events8), events9))

        def eventList9:=
            if (defaultTime(events9) >= timeNow) then
                List.prepend(9, List.empty[Int])
            else
                List.empty[Int]

        def eventList8:=
            if (defaultTime(events8) >= timeNow) then
                List.prepend(8, eventList9)
            else
                eventList9

        def eventList7:=
            if (defaultTime(events7) >= timeNow) then
                List.prepend(7, eventList8)
            else
                eventList8

        def eventList6:=
            if (defaultTime(events6) >= timeNow) then
                List.prepend(6, eventList7)
            else
                eventList7

        def eventList5:=
            if (defaultTime(events5) >= timeNow) then
                List.prepend(5, eventList6)
            else
                eventList6

        def eventList4:=
            if (defaultTime(events4) >= timeNow) then
                List.prepend(4, eventList5)
            else
                eventList5

        def eventList3:=
            if (defaultTime(events3) >= timeNow) then
                List.prepend(3, eventList4)
            else
                eventList4

        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

        StrongSynchronizationConstraintReset(eventList, 9, tolerance, resetTime)
    }

	def synchronizationConstraint10[A, B, C, D, E, F, G, H, I, J](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], events10: Events[J], tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset10(events1, events2, events3, events4, events5, events6, events7, events8,
			events9, events10, tolerance, pseudoInfty)

	def synchronizationConstraint2[A, B](events1: Events[A], events2: Events[B], tolerance: Int
			): Events[fourValuedLogicValue]:=
		synchronizationConstraint2Reset(events1, events2, tolerance, pseudoInfty)

def synchronizationConstraint2Reset[A, B](events1: Events[A], events2: Events[B], tolerance: Int,
			resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(events1, events2))

    def eventList2:=
        if (defaultTime(events2) >= timeNow) then
            List.prepend(2, List.empty[Int])
        else
            List.empty[Int]

    def eventList:=
        if (defaultTime(events1) >= timeNow) then
            List.prepend(1, eventList2)
        else
            eventList2

    synchronizationConstraintReset(eventList, 2, tolerance, resetTime)
}

def synchronizationConstraint3[A, B, C](events1: Events[A], events2: Events[B], events3: Events[C],
			tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset3(events1, events2, events3, tolerance, pseudoInfty)

	def synchronizationConstraint4[A, B, C, D](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset4(events1, events2, events3, events4, tolerance, pseudoInfty)

	def synchronizationConstraint5[A, B, C, D, E](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], events5: Events[E], tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset5(events1, events2, events3, events4, events5, tolerance, pseudoInfty)

	def synchronizationConstraint6[A, B, C, D, E, F](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], events5: Events[E], events6: Events[F], tolerance: Int):
			Events[fourValuedLogicValue]:=
		synchronizationConstraintReset6(events1, events2, events3, events4, events5, events6, tolerance,
			pseudoInfty)

	def synchronizationConstraint7[A, B](events1: Events[A], events2: Events[B], events3: Events[B],
			events4: Events[B], events5: Events[B], events6: Events[B], events7: Events[B], tolerance: Int):
			Events[fourValuedLogicValue]:=
		synchronizationConstraintReset7(events1, events2, events3, events4, events5, events6, events7,
			tolerance, pseudoInfty)

	def synchronizationConstraint8[A, B, C, D, E, F, G, H](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G], events8: Events[H],
			tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset8(events1, events2, events3, events4, events5, events6, events7, events8,
			tolerance, pseudoInfty)

	def synchronizationConstraint9[A, B, C, D, E, F, G, H, I](events1: Events[A], events2: Events[B], events3: Events[C],
			events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G], events8: Events[H],
			events9: Events[I], tolerance: Int): Events[fourValuedLogicValue]:=
		synchronizationConstraintReset9(events1, events2, events3, events4, events5, events6, events7, events8,
			events9, tolerance, pseudoInfty)

	def synchronizationConstraintReset(eventIndices: Events[List[Int]], streamCount: Int, tolerance: Int,
			resetTime: Int): Events[fourValuedLogicValue]:= {

        def buildSynchronizationEventInfo(streamInd: Int, evtTime: Int, flflld: Bool) : SynchronizationEventInfo:=
            {streamIndex= streamInd, eventTime= evtTime, fulfilled= flflld}

        # add events from one timestamp to the state
        # O(|events|)
        def addEvents(existingEvents: List[SynchronizationEventInfo], newEventStreamIndices: List[Int], timeNow: Int) :
                List[SynchronizationEventInfo]:=
            if (List.size(newEventStreamIndices) == 0) then
                existingEvents
            else
                addEvents(List.append(existingEvents,
                        buildSynchronizationEventInfo(List.head(newEventStreamIndices), timeNow, false)),
                    List.tail(newEventStreamIndices), timeNow)

        # checks, if the events between timeNow and (timeNow-tolerance) fulfills the cluster
        # O(List_length)= O(tolerance*|events|)
        def clusterFulfilled(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int,
				streamCount: Int): Bool := {
            # creates a set with [1, 2, ..., size]
            def fillSet(count: Int): Set[Int]:=
                if count == 0 then
                    Set.empty[Int]
                else
                    Set.add(fillSet(count-1), count)

            def checkCluster(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int,
					reaminingIndices: Set[Int]):Bool:=
                if Set.size(reaminingIndices) == 0 then
                    true
                else
                    if (List.size(events) == 0) then
                        false
                    else
                        if (List.head(events).eventTime + tolerance >= timeNow) &&
								(Set.contains(reaminingIndices, List.head(events).streamIndex)) then
							checkCluster(List.tail(events), timeNow, tolerance,
								Set.remove(reaminingIndices, List.head(events).streamIndex))
                        else
                            checkCluster(List.tail(events), timeNow, tolerance, reaminingIndices)

            checkCluster(events, timeNow, tolerance, fillSet(streamCount))
        }


        # sets all Events in list to fulfilled, if not too old
        def setEventsToFulfilled(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int,
				streamCount: Int): List[SynchronizationEventInfo] :=
            if (List.size(events) == 0) then
                events
            else
                # set List.head to fulfilled, if not too old
                List.prepend(
                    if (List.head(events).eventTime + tolerance >= timeNow) then
                        buildSynchronizationEventInfo(List.head(events).streamIndex,
							List.head(events).eventTime, true)
                    else
                        List.head(events),
                    setEventsToFulfilled(List.tail(events), timeNow, tolerance, streamCount))

        #set fulfilled state of events to true, if fulfilled
        def updateFullfilledEvents(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int,
				streamCount: Int): List[SynchronizationEventInfo]:=
            if (clusterFulfilled(events, timeNow, tolerance, streamCount)) then
                setEventsToFulfilled(events, timeNow, tolerance, streamCount)
            else
                events

        # creates a List with all events, that are older than tolerance
        def eventsToRemove(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int):
                List[SynchronizationEventInfo] :=
            if (List.size(events) == 0) then
                events
            else
                # head of List too old
                if(timeNow - List.head(events).eventTime > tolerance) then
                    # add head of list to return list
                    List.append(eventsToRemove(List.tail(events), timeNow, tolerance), List.head(events))
                else
                    # rest of list can't be older-> return empty
                    List.empty[SynchronizationEventInfo]

        # removes all events, that are older than tolerance
        def removeEvents(events: List[SynchronizationEventInfo], timeNow: Int, tolerance: Int):
                List[SynchronizationEventInfo] :=
            if (List.size(events) == 0) then
                events
            else
                # head of List too old
                if(timeNow - List.head(events).eventTime > tolerance) then
                    removeEvents(List.tail(events), timeNow, tolerance)
                else
                    # rest of list can't be older-> return unchanged
                    events

        def noUnfulfilledRemoved(removedEvents: List[SynchronizationEventInfo]) : Bool :=
            if (List.size(removedEvents) == 0) then
                true
            else
                List.head(removedEvents).fulfilled &&
                noUnfulfilledRemoved(List.tail(removedEvents))
        # insert new events and set cluster to fulfilled, if possible
       def storedEventsBeforeRemove: Events[List[SynchronizationEventInfo]] :=
            slift4(slift3(default(last(storedEvents, eventIndices), List.empty[SynchronizationEventInfo]),
					eventIndices, time(eventIndices), addEvents),
				time(eventIndices), tolerance, streamCount, updateFullfilledEvents)
        # remove old events from list
        def storedEvents: Events[List[SynchronizationEventInfo]] :=
            slift3(storedEventsBeforeRemove, time(eventIndices), tolerance, removeEvents)

        def timeOldestUnfulfilledEvent(storedEvents: List[SynchronizationEventInfo]): Int :=
            if (List.size(storedEvents) == 0) then
                pseudoInfty
            else
                if !List.head(storedEvents).fulfilled then
                    List.head(storedEvents).eventTime
                else
                    timeOldestUnfulfilledEvent(List.tail(storedEvents))

        # timestamps, in which the evaluation occurs
        def evaluateTimes = mergeUnit(eventIndices,
            safeDelay(slift1(storedEvents, timeOldestUnfulfilledEvent) + tolerance - time(eventIndices)+1, eventIndices))

		def failingTimeStamps: Events[Unit] =
			filter(evaluateTimes, last(result.final, evaluateTimes) &&
					!(last(last(result.final, evaluateTimes), evaluateTimes)))
		#timestamps, in which the state of the monitor is resetted
		def resets: Events[Unit]=
			delay(const(resetTime, failingTimeStamps)-(time(evaluateTimes) -
					prev(time(evaluateTimes))),
				failingTimeStamps)

        #Evaluation
        #no unfullfilled event-> current true
        def result := stillFulfillableReset(
            if (slift1(storedEvents, timeOldestUnfulfilledEvent) == pseudoInfty) then
                {value= true, final= false}
            else
                #check, if all removed events are fulfilled(had a cluster)-> current false, but not final
                if (slift1(storedEventsBeforeRemove, timeOldestUnfulfilledEvent) >= time(evaluateTimes) - tolerance) then
                    {value= false, final= false}
                else
                    {value= false, final= true},
			resetTime)

		result
    }

def synchronizationConstraintReset10[A, B, C, D, E, F, G, H, I, J](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], events10: Events[J], tolerance: Int, resetTime: Int):
			Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5), events6), events7), events8), events9), events10))

    def eventList10:=
        if (defaultTime(events10) >= timeNow) then
            List.prepend(10, List.empty[Int])
        else
            List.empty[Int]

    def eventList9:=
        if (defaultTime(events9) >= timeNow) then
            List.prepend(9, eventList10)
        else
            eventList10

    def eventList8:=
        if (defaultTime(events8) >= timeNow) then
            List.prepend(8, eventList9)
        else
            eventList9

    def eventList7:=
        if (defaultTime(events7) >= timeNow) then
            List.prepend(7, eventList8)
        else
            eventList8

    def eventList6:=
        if (defaultTime(events6) >= timeNow) then
            List.prepend(6, eventList7)
        else
            eventList7

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, eventList6)
        else
            eventList6

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 10, tolerance, resetTime)
}

	def synchronizationConstraintReset3[A, B, C](events1: Events[A], events2: Events[B], events3: Events[C],
			tolerance: Int, ResetTime: Int): Events[fourValuedLogicValue]:={
        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

        synchronizationConstraintReset(eventList, 3, tolerance, ResetTime)
    }

def synchronizationConstraintReset4[A, B, C, D](events1: Events[A], events2: Events[B], events3: Events[C],
        events4: Events[D], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(events1, events2), events3), events4))

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, List.empty[Int])
        else
            List.empty[Int]

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 4, tolerance, resetTime)
}

def synchronizationConstraintReset5[A, B, C, D, E](events1: Events[A], events2: Events[B], events3: Events[C],
        events4: Events[D], events5: Events[E], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5))

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, List.empty[Int])
        else
            List.empty[Int]

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 5, tolerance, resetTime)
}

def synchronizationConstraintReset6[A, B, C, D, E, F](events1: Events[A], events2: Events[B],
        events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], tolerance: Int,
			resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5), events6))

    def eventList6:=
        if (defaultTime(events6) >= timeNow) then
            List.prepend(6, List.empty[Int])
        else
            List.empty[Int]

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, eventList6)
        else
            eventList6

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 6, tolerance, resetTime)
}

def synchronizationConstraintReset7[A, B, C, D, E, F, G](events1: Events[A], events2: Events[B], events3:
			Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5), events6), events7))

    def eventList7:=
        if (defaultTime(events7) >= timeNow) then
            List.prepend(7, List.empty[Int])
        else
            List.empty[Int]

    def eventList6:=
        if (defaultTime(events6) >= timeNow) then
            List.prepend(6, eventList7)
        else
            eventList7

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, eventList6)
        else
            eventList6

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 7, tolerance, resetTime)
}

def synchronizationConstraintReset8[A, B, C, D, E, F, G, H](events1: Events[A], events2: Events[B], events3:
			Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G], events8:
			Events[H], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={
    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5), events6), events7), events8))

    def eventList8:=
        if (defaultTime(events8) >= timeNow) then
            List.prepend(8, List.empty[Int])
        else
            List.empty[Int]

    def eventList7:=
        if (defaultTime(events7) >= timeNow) then
            List.prepend(7, eventList8)
        else
            eventList8

    def eventList6:=
        if (defaultTime(events6) >= timeNow) then
            List.prepend(6, eventList7)
        else
            eventList7

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, eventList6)
        else
            eventList6

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 8, tolerance, resetTime)
}

def synchronizationConstraintReset9[A, B, C, D, E, F, G, H, I](events1: Events[A], events2: Events[B],
			events3: Events[C], events4: Events[D], events5: Events[E], events6: Events[F], events7: Events[G],
			events8: Events[H], events9: Events[I], tolerance: Int, resetTime: Int): Events[fourValuedLogicValue]:={

    def timeNow: Events[Int] := time(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(mergeUnit(
        events1, events2), events3), events4), events5), events6), events7), events8), events9))

    def eventList9:=
        if (defaultTime(events9) >= timeNow) then
            List.prepend(9, List.empty[Int])
        else
            List.empty[Int]

    def eventList8:=
        if (defaultTime(events8) >= timeNow) then
            List.prepend(8, eventList9)
        else
            eventList9

    def eventList7:=
        if (defaultTime(events7) >= timeNow) then
            List.prepend(7, eventList8)
        else
            eventList8

    def eventList6:=
        if (defaultTime(events6) >= timeNow) then
            List.prepend(6, eventList7)
        else
            eventList7

    def eventList5:=
        if (defaultTime(events5) >= timeNow) then
            List.prepend(5, eventList6)
        else
            eventList6

    def eventList4:=
        if (defaultTime(events4) >= timeNow) then
            List.prepend(4, eventList5)
        else
            eventList5

    def eventList3:=
        if (defaultTime(events3) >= timeNow) then
            List.prepend(3, eventList4)
        else
            eventList4

    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

    synchronizationConstraintReset(eventList, 9, tolerance, resetTime)
}