/
pacemakerSL.vdmsl.result
1 lines (1 loc) · 19.2 KB
/
pacemakerSL.vdmsl.result
1
["type compatibility obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 547:1: (forall t:PacemakerDDD`Time, r:PacemakerDDD`ReactionTimeline, AA:PacemakerDDD`Alarm, VA:PacemakerDDD`Alarm, LastA:PacemakerDDD`Time, LastV:PacemakerDDD`Time \u0026 is_((if (((t - LastA) \u003c ARP) or ((VA \u003e 0) or ((t - LastA) \u003c PVARP)))\nthen SensedNothing(t, r, AA, VA, LastA, LastV)\nelse mk_(r, 0, (t + AVD), t, LastV)), (PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time)))","legal map application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 456:55: (forall mk_(-, acc, time):(PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time), oldstate:PacemakerAOOR`Sigma \u0026 (true \u003d\u003e (time in set (dom rateChangePlan))))","legal sequence application obligation in \u0027PacemakerAAI\u0027 (pacemakerSL.vdmsl) at line 74:37: (forall inp:PacemakerAAI`SenseTimeline \u0026 (exists r:PacemakerAAI`ReactionTimeline \u0026 (forall i in set (inds r) \u0026 (i in set (inds r)))))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 485:28: inv_AccelerometerData(1)","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 494:22: is_((((([mk_(\u003cNONE\u003e, nil, i) | i in set {1, ... ,120}] ^ [mk_(\u003cNONE\u003e, HIGH, 121)]) ^ [mk_(\u003cNONE\u003e, nil, i) | i in set {121, ... ,190}]) ^ [mk_(\u003cNONE\u003e, LOW, 191)]) ^ [mk_(\u003cNONE\u003e, nil, i) | i in set {192, ... ,436}]), seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)))","type invariant satisfiable obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 414:1: (exists n:PacemakerAOOR`AccelerometerData \u0026 (n \u003c 3))","non-zero obligation in \u0027PacemakerAAI\u0027 (pacemakerSL.vdmsl) at line 81:65: (forall inp:PacemakerAAI`SenseTimeline \u0026 (exists r:PacemakerAAI`ReactionTimeline \u0026 let m:set of (nat1) \u003d {i | i in set (inds r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in (((len r) \u003d (len inp)) \u003d\u003e ((r(1) \u003d \u003cPULSE\u003e) \u003d\u003e (forall x in set m \u0026 ((exists y in set m \u0026 (y \u003e x)) \u003d\u003e (forall z in set m \u0026 ((z \u003e\u003d x) \u003d\u003e (LRL \u003c\u003e 0)))))))))","legal map application obligation in \u0027PacemakerAOO\u0027 (pacemakerSL.vdmsl) at line 331:29: (forall inp:PacemakerAOO`SenseTimeline \u0026 (exists r:PacemakerAOO`ReactionTimeline \u0026 let m:set of (PacemakerAOO`Time) \u003d {i | i in set (dom r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in ((((card (dom r)) \u003d (card (dom inp))) and ((card (dom inp)) \u003e 1)) \u003d\u003e (1 in set (dom r)))))","type invariant satisfiable obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 758:1: (exists ppm:RateController`PPM \u0026 ((ppm \u003e\u003d 30) and (ppm \u003c\u003d 175)))","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 783:31: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 ((out(t) \u003d MSR) \u003d\u003e ((t - ReactionTime) in set (dom inp)))))))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 412:56: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in ((l(1) \u003d HIGH) \u003d\u003e (forall i in set (inds l) \u0026 (inv_AccelerometerData(l(i)) and is_(l(i), nat)))))","function postcondition satisfiable obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 780:1: (forall inp:RateController`Input \u0026 (pre_Simulate(inp) \u003d\u003e (exists out:RateController`Output \u0026 post_Simulate(inp, out))))","non-zero obligation in \u0027PacemakerDOO\u0027 (pacemakerSL.vdmsl) at line 662:23: (forall mk_(inp, n):(PacemakerDOO`SensedTimeline * nat1) \u0026 (exists r:PacemakerDOO`ReactionTimeline \u0026 let nPulsesAtria:nat \u003d (card {i | i in set r \u0026 ((i.#1) \u003d \u003cATRIA\u003e)}), nPulsesVentricle:nat \u003d (card {i | i in set r \u0026 ((i.#1) \u003d \u003cVENTRICLE\u003e)}) in (n \u003c\u003e 0)))","recursive function obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 541:44: (forall mk_(i, t, s, r, AA, VA, LastA, LastV):(PacemakerDDD`Time * PacemakerDDD`Time * PacemakerDDD`SenseTimeline * PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time) \u0026 ((not (i \u003d t)) \u003d\u003e ((mk_(i, \u003cATRIUM\u003e) in set s) \u003d\u003e (measure_PM(mk_(i, t, s, r, AA, VA, LastA, LastV)) \u003e measure_PM(c((i + 1), t, s, SensedAtrium(i, r, AA, VA, LastA, LastV)))))))","legal sequence application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 412:56: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in ((l(1) \u003d HIGH) \u003d\u003e (forall i in set (inds l) \u0026 (i in set (inds l)))))","function postcondition satisfiable obligation in \u0027PacemakerAOO\u0027 (pacemakerSL.vdmsl) at line 327:1: (forall inp:PacemakerAOO`SenseTimeline \u0026 (exists r:PacemakerAOO`ReactionTimeline \u0026 post_Pacemaker(inp, r)))","recursive function obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 544:48: (forall mk_(i, t, s, r, AA, VA, LastA, LastV):(PacemakerDDD`Time * PacemakerDDD`Time * PacemakerDDD`SenseTimeline * PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time) \u0026 ((not (i \u003d t)) \u003d\u003e ((not (mk_(i, \u003cATRIUM\u003e) in set s)) \u003d\u003e ((not (mk_(i, \u003cVENTRICLE\u003e) in set s)) \u003d\u003e (measure_PM(mk_(i, t, s, r, AA, VA, LastA, LastV)) \u003e measure_PM(c((i + 1), t, s, SensedNothing(i, r, AA, VA, LastA, LastV))))))))","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 768:26: inv_PPM(120)","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 786:36: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (((out(t) \u003d MSR) \u003d\u003e ((inp((t - ReactionTime)) \u003e Threshold) or (out((t - 1)) \u003d MSR))) \u003d\u003e (forall t in set ((dom inp) \\ {1}) \u0026 ((out(t) \u003d LRL) \u003d\u003e is_((t - RecoveryTime), nat1))))))))","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 786:66: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (((out(t) \u003d MSR) \u003d\u003e ((inp((t - ReactionTime)) \u003e Threshold) or (out((t - 1)) \u003d MSR))) \u003d\u003e (forall t in set ((dom inp) \\ {1}) \u0026 ((out(t) \u003d LRL) \u003d\u003e ((not (inp((t - RecoveryTime)) \u003c Threshold)) \u003d\u003e ((t - 1) in set (dom out))))))))))","legal sequence application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 412:70: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in ((l(1) \u003d HIGH) \u003d\u003e (forall i in set (inds l) \u0026 ((l(i) \u003c MED) \u003d\u003e ((i - 1) in set (inds l))))))","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 786:14: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (((out(t) \u003d MSR) \u003d\u003e ((inp((t - ReactionTime)) \u003e Threshold) or (out((t - 1)) \u003d MSR))) \u003d\u003e (forall t in set ((dom inp) \\ {1}) \u0026 (t in set (dom out))))))))","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 786:71: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (((out(t) \u003d MSR) \u003d\u003e ((inp((t - ReactionTime)) \u003e Threshold) or (out((t - 1)) \u003d MSR))) \u003d\u003e (forall t in set ((dom inp) \\ {1}) \u0026 ((out(t) \u003d LRL) \u003d\u003e ((not (inp((t - RecoveryTime)) \u003c Threshold)) \u003d\u003e is_((t - 1), nat1)))))))))","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 783:66: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 ((out(t) \u003d MSR) \u003d\u003e ((not (inp((t - ReactionTime)) \u003e Threshold)) \u003d\u003e ((t - 1) in set (dom out))))))))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 412:70: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in ((l(1) \u003d HIGH) \u003d\u003e (forall i in set (inds l) \u0026 ((l(i) \u003c MED) \u003d\u003e (inv_AccelerometerData(l((i - 1))) and is_(l((i - 1)), nat))))))","type invariant satisfiable obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 739:1: (exists a:RateController`ActivityData \u0026 (a \u003c\u003d 7))","type compatibility obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 555:1: (forall t:PacemakerDDD`Time, r:PacemakerDDD`ReactionTimeline, AA:PacemakerDDD`Alarm, VA:PacemakerDDD`Alarm, LastA:PacemakerDDD`Time, LastV:PacemakerDDD`Time \u0026 is_((if ((t - LastV) \u003c VRP)\nthen SensedNothing(t, r, AA, VA, LastA, LastV)\nelse mk_(r, (t + VAD), 0, LastA, t)), (PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time)))","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 783:71: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 ((out(t) \u003d MSR) \u003d\u003e ((not (inp((t - ReactionTime)) \u003e Threshold)) \u003d\u003e is_((t - 1), nat1)))))))","non-empty sequence obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 450:57: (forall inp:PacemakerAOOR`SenseTimeline, oldstate:PacemakerAOOR`Sigma \u0026 ((not (inp \u003d [])) \u003d\u003e (inp \u003c\u003e [])))","recursive function obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 543:48: (forall mk_(i, t, s, r, AA, VA, LastA, LastV):(PacemakerDDD`Time * PacemakerDDD`Time * PacemakerDDD`SenseTimeline * PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time) \u0026 ((not (i \u003d t)) \u003d\u003e ((not (mk_(i, \u003cATRIUM\u003e) in set s)) \u003d\u003e ((mk_(i, \u003cVENTRICLE\u003e) in set s) \u003d\u003e (measure_PM(mk_(i, t, s, r, AA, VA, LastA, LastV)) \u003e measure_PM(c((i + 1), t, s, SensedVentricle(i, r, AA, VA, LastA, LastV))))))))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 486:28: inv_AccelerometerData(0)","legal sequence application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 411:53: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 (forall i in set (inds stl) \u0026 (i in set (inds stl))))","type invariant satisfiable obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 410:1: (exists stl:PacemakerAOOR`SenseTimeline \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in ((l(1) \u003d HIGH) and (forall i in set (inds l) \u0026 ((l(i) \u003c MED) \u003d\u003e (l((i - 1)) \u003e MED)))))","legal sequence application obligation in \u0027PacemakerAAI\u0027 (pacemakerSL.vdmsl) at line 83:74: (forall inp:PacemakerAAI`SenseTimeline \u0026 (exists r:PacemakerAAI`ReactionTimeline \u0026 let m:set of (nat1) \u003d {i | i in set (inds r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in (((len r) \u003d (len inp)) \u003d\u003e ((r(1) \u003d \u003cPULSE\u003e) \u003d\u003e (forall x in set m \u0026 ((exists y in set m \u0026 (y \u003e x)) \u003d\u003e ((not (exists z in set m \u0026 ((z \u003e\u003d x) and ((z - x) \u003c\u003d (60000 / LRL))))) \u003d\u003e (forall z in set (inds inp) \u0026 ((z \u003e\u003d x) \u003d\u003e (((z - x) \u003e ARP) \u003d\u003e (z in set (inds inp))))))))))))","type invariant satisfiable obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 747:1: (exists rf:RateController`RF \u0026 (rf \u003c\u003d 16))","non-zero obligation in \u0027PacemakerAOO\u0027 (pacemakerSL.vdmsl) at line 335:58: (forall inp:PacemakerAOO`SenseTimeline \u0026 (exists r:PacemakerAOO`ReactionTimeline \u0026 let m:set of (PacemakerAOO`Time) \u003d {i | i in set (dom r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in ((((card (dom r)) \u003d (card (dom inp))) and ((card (dom inp)) \u003e 1)) \u003d\u003e ((r(1) \u003d \u003cPULSE\u003e) \u003d\u003e (forall x in set m \u0026 ((exists y in set m \u0026 (y \u003e x)) \u003d\u003e (forall y in set m \u0026 (LRL \u003c\u003e 0))))))))","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 783:14: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (t in set (dom out))))))","function postcondition satisfiable obligation in \u0027PacemakerDOO\u0027 (pacemakerSL.vdmsl) at line 659:1: (forall mk_(inp, n):(PacemakerDOO`SensedTimeline * nat1) \u0026 (exists r:PacemakerDOO`ReactionTimeline \u0026 post_Pacemaker(mk_(inp, n), r)))","function postcondition satisfiable obligation in \u0027PacemakerAAI\u0027 (pacemakerSL.vdmsl) at line 73:1: (forall inp:PacemakerAAI`SenseTimeline \u0026 (exists r:PacemakerAAI`ReactionTimeline \u0026 post_Pacemaker(inp, r)))","type compatibility obligation in \u0027PacemakerDDD\u0027 (pacemakerSL.vdmsl) at line 563:1: (forall t:PacemakerDDD`Time, r:PacemakerDDD`ReactionTimeline, AA:PacemakerDDD`Alarm, VA:PacemakerDDD`Alarm, LastA:PacemakerDDD`Time, LastV:PacemakerDDD`Time \u0026 is_((if ((AA \u003e 0) and (t \u003e\u003d AA))\nthen mk_((r union {mk_(t, \u003cATRIUM\u003e)}), 0, (t + AVD), t, LastV)\nelseif ((VA \u003e 0) and (t \u003e\u003d VA))\nthen mk_((r union {mk_(t, \u003cVENTRICLE\u003e)}), (t + VAD), 0, LastA, t)\nelse mk_(r, AA, VA, LastA, LastV)), (PacemakerDDD`ReactionTimeline * PacemakerDDD`Alarm * PacemakerDDD`Alarm * PacemakerDDD`Time * PacemakerDDD`Time)))","non-empty sequence obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 450:36: (forall inp:PacemakerAOOR`SenseTimeline, oldstate:PacemakerAOOR`Sigma \u0026 ((not (inp \u003d [])) \u003d\u003e (inp \u003c\u003e [])))","legal map application obligation in \u0027PacemakerAOO\u0027 (pacemakerSL.vdmsl) at line 328:36: (forall inp:PacemakerAOO`SenseTimeline \u0026 (exists r:PacemakerAOO`ReactionTimeline \u0026 (forall i in set (dom r) \u0026 (i in set (dom r)))))","non-zero obligation in \u0027PacemakerDOO\u0027 (pacemakerSL.vdmsl) at line 664:27: (forall mk_(inp, n):(PacemakerDOO`SensedTimeline * nat1) \u0026 (exists r:PacemakerDOO`ReactionTimeline \u0026 let nPulsesAtria:nat \u003d (card {i | i in set r \u0026 ((i.#1) \u003d \u003cATRIA\u003e)}), nPulsesVentricle:nat \u003d (card {i | i in set r \u0026 ((i.#1) \u003d \u003cVENTRICLE\u003e)}) in (((nPulsesAtria / n) \u003e\u003d ((LRL / 60) / 1000)) \u003d\u003e (n \u003c\u003e 0))))","legal sequence application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 411:21: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 (forall i in set (inds stl) \u0026 (((stl(i).#2) \u003c\u003e nil) \u003d\u003e (i in set (inds stl)))))","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 769:35: inv_ActivityData(6)","legal sequence application obligation in \u0027PacemakerAAI\u0027 (pacemakerSL.vdmsl) at line 77:9: (forall inp:PacemakerAAI`SenseTimeline \u0026 (exists r:PacemakerAAI`ReactionTimeline \u0026 let m:set of (nat1) \u003d {i | i in set (inds r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in (((len r) \u003d (len inp)) \u003d\u003e (1 in set (inds r)))))","non-zero obligation in \u0027PacemakerAAT\u0027 (pacemakerSL.vdmsl) at line 196:65: (forall inp:PacemakerAAT`SenseTimeline \u0026 (exists r:PacemakerAAT`ReactionTimeline \u0026 let m:set of (nat1) \u003d {i | i in set (inds r) \u0026 (r(i) \u003d \u003cPULSE\u003e)} in (((len r) \u003d (len inp)) \u003d\u003e (forall x in set m \u0026 ((exists y in set m \u0026 (y \u003e x)) \u003d\u003e (forall z in set m \u0026 ((z \u003e\u003d x) \u003d\u003e (LRL \u003c\u003e 0))))))))","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 771:25: inv_RF(8)","legal map application obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 786:31: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 (((out(t) \u003d MSR) \u003d\u003e ((inp((t - ReactionTime)) \u003e Threshold) or (out((t - 1)) \u003d MSR))) \u003d\u003e (forall t in set ((dom inp) \\ {1}) \u0026 ((out(t) \u003d LRL) \u003d\u003e ((t - RecoveryTime) in set (dom inp)))))))))","legal sequence application obligation in \u0027PacemakerAAT\u0027 (pacemakerSL.vdmsl) at line 191:37: (forall inp:PacemakerAAT`SenseTimeline \u0026 (exists r:PacemakerAAT`ReactionTimeline \u0026 (forall i in set (inds r) \u0026 (i in set (inds r)))))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 488:28: inv_AccelerometerData(2)","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 783:36: (forall inp:RateController`Input \u0026 ((0 not in set (dom inp)) \u003d\u003e (exists out:RateController`Output \u0026 (forall t in set (dom inp) \u0026 ((out(t) \u003d MSR) \u003d\u003e is_((t - ReactionTime), nat1))))))","legal sequence application obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 412:15: (forall stl:seq of ((PacemakerAOOR`Sense * [PacemakerAOOR`AccelerometerData] * PacemakerAOOR`Time)) \u0026 let l:seq of ([PacemakerAOOR`AccelerometerData]) \u003d [(stl(i).#2) | i in set (inds stl) \u0026 ((stl(i).#2) \u003c\u003e nil)] in (1 in set (inds l)))","type compatibility obligation in \u0027PacemakerAOOR\u0027 (pacemakerSL.vdmsl) at line 487:28: inv_AccelerometerData(1)","type compatibility obligation in \u0027RateController\u0027 (pacemakerSL.vdmsl) at line 767:26: inv_PPM(60)","function postcondition satisfiable obligation in \u0027PacemakerAAT\u0027 (pacemakerSL.vdmsl) at line 190:1: (forall inp:PacemakerAAT`SenseTimeline \u0026 (exists r:PacemakerAAT`ReactionTimeline \u0026 post_Pacemaker(inp, r)))"]