Specifications

A minimalist clock that produces a value periodically without an input.

Input streams: None.

Output stream: The periodic ticker clock.

time domain Double
output TimeDiff clock:
  ticks = {0} U delay clock
  val = 5
{"id":"clock","timestamp":0,"value":5}
{"id":"clock","timestamp":5,"value":5}
{"id":"clock","timestamp":10,"value":5}
{"id":"clock","timestamp":15,"value":5}
{"id":"clock","timestamp":20,"value":5}
{"id":"clock","timestamp":25,"value":5}
{"id":"clock","timestamp":30,"value":5}
{"id":"clock","timestamp":35,"value":5}
{"id":"clock","timestamp":40,"value":5}
{"id":"clock","timestamp":45,"value":5}
{"id":"clock","timestamp":50,"value":5}
{"id":"clock","timestamp":55,"value":5}
{"id":"clock","timestamp":60,"value":5}
{"id":"clock","timestamp":65,"value":5}
{"id":"clock","timestamp":70,"value":5}
{"id":"clock","timestamp":75,"value":5}
{"id":"clock","timestamp":80,"value":5}
{"id":"clock","timestamp":85,"value":5}
{"id":"clock","timestamp":90,"value":5}
{"id":"clock","timestamp":95,"value":5}
{"id":"clock","timestamp":100,"value":5}
...

This example calculates the accumulated energy cost incurred by a monitor, based on a cost model for:

Input streams: A unit value whenever there is an event.

Output stream: The accumulated cost.

time domain Double
use haskell Data.Maybe


#HASKELL
data RunMode = Alert | Sleeping  deriving (Show,Generic,ToJSON,Eq)

type Cost = Int

data CostTable = CT {
  alertPatience :: TimeDiff,
  alertPerSecond :: Cost,
  sleepingPerSecond :: Cost,
  processEvent :: Cost,
  wakeUp :: Cost,
  gotoSleep :: Cost}

runCostPerSecond :: RunMode -> Cost
runCostPerSecond Alert = alertPerSecond ct
runCostPerSecond Sleeping = sleepingPerSecond ct

transitionCost :: RunMode -> RunMode -> Cost
transitionCost Alert Alert = processEvent ct -- Cost of processing an event
transitionCost Sleeping Alert = wakeUp ct + processEvent ct -- Wakeup + processing
transitionCost Alert Sleeping = gotoSleep ct -- Cost of going to sleep
transitionCost Sleeping Sleeping = error "going to sleep while sleeping?" -- This should never happen
#ENDOFHASKELL


const ct = CT 10 100 1 20 100 100
const patience = alertPatience ct

input () wakeup

define TimeDiff sleep_delayer:
  ticks = ticksOf wakeup
  val = 'patience

define () sleep:
  ticks = delay sleep_delayer
  val = '()

define RunMode runMode:
  ticks = ticksOf wakeup U ticksOf sleep
  val = if 1'isJust (fst cv) then 'Alert else 'Sleeping

output Cost cost:
  ticks = ticksOf runMode
  val = let
    previousRunMode = runMode[<t|Alert]
    currentRunMode = cv
    costOfTransitioning = 2'transitionCost previousRunMode currentRunMode
    getTimeT (T x) _ = x
    getTimeT _ y = y
    prevt = 2'getTimeT (timeOf (runMode << t)) now
    timediff = 1'(round.realToFrac) (2'tDiff now prevt)
    accum = cost [<t|0] + timediff * ('runCostPerSecond previousRunMode)
    in
    accum + costOfTransitioning
{"Time": 1, "Value": []}
{"Time": 15, "Value": []}
{"Time": 17, "Value": []}
{"Time": 38, "Value": []}
{"Time": 51, "Value": []}
{"Time": 54, "Value": []}
{"Time": 55, "Value": []}
{"Time": 92, "Value": []}
{"Time": 96, "Value": []}
{"Time": 103, "Value": []}
{"Time": 112, "Value": []}
{"Time": 116, "Value": []}
{"Time": 118, "Value": []}
{"Time": 119, "Value": []}
{"Time": 120, "Value": []}
{"Time": 125, "Value": []}
{"Time": 136, "Value": []}
{"Time": 166, "Value": []}
{"Time": 179, "Value": []}
{"Time": 192, "Value": []}
{"Time": 201, "Value": []}
{"Time": 203, "Value": []}
{"Time": 204, "Value": []}
{"Time": 210, "Value": []}
{"Time": 217, "Value": []}
{"Time": 222, "Value": []}
{"Time": 223, "Value": []}
{"Time": 224, "Value": []}
{"Time": 231, "Value": []}
{"Time": 254, "Value": []}
{"Time": 270, "Value": []}
{"Time": 272, "Value": []}
{"Time": 284, "Value": []}
{"Time": 289, "Value": []}
{"Time": 305, "Value": []}
{"Time": 317, "Value": []}
{"Time": 318, "Value": []}
{"Time": 327, "Value": []}
{"Time": 330, "Value": []}
{"Time": 347, "Value": []}
{"Time": 349, "Value": []}
{"Time": 396, "Value": []}
{"Time": 404, "Value": []}
{"Time": 409, "Value": []}
{"Time": 415, "Value": []}
{"Time": 416, "Value": []}
{"Time": 439, "Value": []}
{"Time": 465, "Value": []}
{"Time": 469, "Value": []}
{"Time": 479, "Value": []}
{"Time": 495, "Value": []}
{"id":"cost","timestamp":1,"value":20}
{"id":"cost","timestamp":11,"value":1120}
{"id":"cost","timestamp":15,"value":1244}
{"id":"cost","timestamp":17,"value":1464}
{"id":"cost","timestamp":27,"value":2564}
{"id":"cost","timestamp":38,"value":2695}
{"id":"cost","timestamp":48,"value":3795}
{"id":"cost","timestamp":51,"value":3918}
{"id":"cost","timestamp":54,"value":4238}
{"id":"cost","timestamp":55,"value":4358}
{"id":"cost","timestamp":65,"value":5458}
{"id":"cost","timestamp":92,"value":5605}
{"id":"cost","timestamp":96,"value":6025}
{"id":"cost","timestamp":103,"value":6745}
{"id":"cost","timestamp":112,"value":7665}
{"id":"cost","timestamp":116,"value":8085}
{"id":"cost","timestamp":118,"value":8305}
{"id":"cost","timestamp":119,"value":8425}
{"id":"cost","timestamp":120,"value":8545}
{"id":"cost","timestamp":125,"value":9065}
{"id":"cost","timestamp":135,"value":10165}
{"id":"cost","timestamp":136,"value":10286}
{"id":"cost","timestamp":146,"value":11386}
{"id":"cost","timestamp":166,"value":11526}
{"id":"cost","timestamp":176,"value":12626}
{"id":"cost","timestamp":179,"value":12749}
{"id":"cost","timestamp":189,"value":13849}
{"id":"cost","timestamp":192,"value":13972}
{"id":"cost","timestamp":201,"value":14892}
{"id":"cost","timestamp":203,"value":15112}
{"id":"cost","timestamp":204,"value":15232}
{"id":"cost","timestamp":210,"value":15852}
{"id":"cost","timestamp":217,"value":16572}
{"id":"cost","timestamp":222,"value":17092}
{"id":"cost","timestamp":223,"value":17212}
{"id":"cost","timestamp":224,"value":17332}
{"id":"cost","timestamp":231,"value":18052}
{"id":"cost","timestamp":241,"value":19152}
{"id":"cost","timestamp":254,"value":19285}
{"id":"cost","timestamp":264,"value":20385}
{"id":"cost","timestamp":270,"value":20511}
{"id":"cost","timestamp":272,"value":20731}
{"id":"cost","timestamp":282,"value":21831}
{"id":"cost","timestamp":284,"value":21953}
{"id":"cost","timestamp":289,"value":22473}
{"id":"cost","timestamp":299,"value":23573}
{"id":"cost","timestamp":305,"value":23699}
{"id":"cost","timestamp":315,"value":24799}
{"id":"cost","timestamp":317,"value":24921}
{"id":"cost","timestamp":318,"value":25041}
{"id":"cost","timestamp":327,"value":25961}
{"id":"cost","timestamp":330,"value":26281}
{"id":"cost","timestamp":340,"value":27381}
{"id":"cost","timestamp":347,"value":27508}
{"id":"cost","timestamp":349,"value":27728}
{"id":"cost","timestamp":359,"value":28828}
{"id":"cost","timestamp":396,"value":28985}
{"id":"cost","timestamp":404,"value":29805}
{"id":"cost","timestamp":409,"value":30325}
{"id":"cost","timestamp":415,"value":30945}
{"id":"cost","timestamp":416,"value":31065}
{"id":"cost","timestamp":426,"value":32165}
{"id":"cost","timestamp":439,"value":32298}
{"id":"cost","timestamp":449,"value":33398}
{"id":"cost","timestamp":465,"value":33534}
{"id":"cost","timestamp":469,"value":33954}
{"id":"cost","timestamp":479,"value":34974}
{"id":"cost","timestamp":489,"value":36074}
{"id":"cost","timestamp":495,"value":36200}
{"id":"cost","timestamp":505,"value":37300}
{"PosOutside":true,"id":"cost"}

This example calculates the stock of a certain product based on two input event streams that represents the sales and arrivals of such product.

Input streams: The sale and arrival streams.

Output stream: The current stock of the product.

time domain Double
use haskell Data.Maybe

input Int sale
input Int arrival

output Int stock:
  ticks = ticksOf sale U ticksOf arrival
  val = let
    (msal, marr) = cv
    sal = 1'(fromMaybe 0) msal
    arr = 1'(fromMaybe 0) marr
    in
    stock[<t|0] - sal + arr
{"Time": 4, "Value": 639}
{"Time": 16, "Value": 653}
{"Time": 44, "Value": 905}
{"Time": 55, "Value": 960}
{"Time": 60, "Value": 663}
{"Time": 82, "Value": 591}
{"Time": 95, "Value": 748}
{"Time": 113, "Value": 707}
{"Time": 121, "Value": 757}
{"Time": 122, "Value": 589}
{"Time": 123, "Value": 704}
{"Time": 127, "Value": 819}
{"Time": 143, "Value": 566}
{"Time": 151, "Value": 982}
{"Time": 170, "Value": 852}
{"Time": 174, "Value": 536}
{"Time": 197, "Value": 1000}
{"Time": 202, "Value": 954}
{"Time": 206, "Value": 555}
{"Time": 216, "Value": 754}
{"Time": 220, "Value": 576}
{"Time": 221, "Value": 683}
{"Time": 224, "Value": 782}
{"Time": 233, "Value": 626}
{"Time": 239, "Value": 786}
{"Time": 243, "Value": 654}
{"Time": 264, "Value": 835}
{"Time": 265, "Value": 592}
{"Time": 282, "Value": 562}
{"Time": 285, "Value": 970}
{"Time": 296, "Value": 504}
{"Time": 308, "Value": 573}
{"Time": 310, "Value": 688}
{"Time": 316, "Value": 732}
{"Time": 322, "Value": 928}
{"Time": 354, "Value": 604}
{"Time": 365, "Value": 711}
{"Time": 366, "Value": 860}
{"Time": 369, "Value": 837}
{"Time": 374, "Value": 514}
{"Time": 387, "Value": 951}
{"Time": 390, "Value": 844}
{"Time": 403, "Value": 752}
{"Time": 426, "Value": 980}
{"Time": 436, "Value": 817}
{"Time": 449, "Value": 672}
{"Time": 475, "Value": 644}
{"Time": 480, "Value": 577}
{"Time": 482, "Value": 791}
{"Time": 493, "Value": 558}
{"Time": 6, "Value": 548}
{"Time": 14, "Value": 711}
{"Time": 16, "Value": 853}
{"Time": 34, "Value": 856}
{"Time": 48, "Value": 898}
{"Time": 64, "Value": 955}
{"Time": 68, "Value": 687}
{"Time": 84, "Value": 845}
{"Time": 86, "Value": 690}
{"Time": 96, "Value": 902}
{"Time": 127, "Value": 628}
{"Time": 134, "Value": 691}
{"Time": 145, "Value": 572}
{"Time": 151, "Value": 937}
{"Time": 155, "Value": 558}
{"Time": 160, "Value": 826}
{"Time": 165, "Value": 648}
{"Time": 178, "Value": 571}
{"Time": 186, "Value": 961}
{"Time": 216, "Value": 975}
{"Time": 227, "Value": 531}
{"Time": 229, "Value": 605}
{"Time": 230, "Value": 994}
{"Time": 231, "Value": 858}
{"Time": 239, "Value": 938}
{"Time": 242, "Value": 679}
{"Time": 244, "Value": 570}
{"Time": 254, "Value": 703}
{"Time": 256, "Value": 899}
{"Time": 273, "Value": 894}
{"Time": 298, "Value": 797}
{"Time": 307, "Value": 886}
{"Time": 317, "Value": 889}
{"Time": 329, "Value": 700}
{"Time": 336, "Value": 736}
{"Time": 342, "Value": 719}
{"Time": 356, "Value": 602}
{"Time": 361, "Value": 912}
{"Time": 367, "Value": 596}
{"Time": 387, "Value": 868}
{"Time": 402, "Value": 808}
{"Time": 410, "Value": 563}
{"Time": 423, "Value": 673}
{"Time": 456, "Value": 707}
{"Time": 476, "Value": 567}
{"Time": 483, "Value": 998}
{"Time": 489, "Value": 696}
{"Time": 491, "Value": 788}
{"Time": 492, "Value": 924}
{"Time": 496, "Value": 621}
{"id":"stock","timestamp":4,"value":-639}
{"id":"stock","timestamp":6,"value":-91}
{"id":"stock","timestamp":14,"value":620}
{"id":"stock","timestamp":16,"value":820}
{"id":"stock","timestamp":34,"value":1676}
{"id":"stock","timestamp":44,"value":771}
{"id":"stock","timestamp":48,"value":1669}
{"id":"stock","timestamp":55,"value":709}
{"id":"stock","timestamp":60,"value":46}
{"id":"stock","timestamp":64,"value":1001}
{"id":"stock","timestamp":68,"value":1688}
{"id":"stock","timestamp":82,"value":1097}
{"id":"stock","timestamp":84,"value":1942}
{"id":"stock","timestamp":86,"value":2632}
{"id":"stock","timestamp":95,"value":1884}
{"id":"stock","timestamp":96,"value":2786}
{"id":"stock","timestamp":113,"value":2079}
{"id":"stock","timestamp":121,"value":1322}
{"id":"stock","timestamp":122,"value":733}
{"id":"stock","timestamp":123,"value":29}
{"id":"stock","timestamp":127,"value":-162}
{"id":"stock","timestamp":134,"value":529}
{"id":"stock","timestamp":143,"value":-37}
{"id":"stock","timestamp":145,"value":535}
{"id":"stock","timestamp":151,"value":490}
{"id":"stock","timestamp":155,"value":1048}
{"id":"stock","timestamp":160,"value":1874}
{"id":"stock","timestamp":165,"value":2522}
{"id":"stock","timestamp":170,"value":1670}
{"id":"stock","timestamp":174,"value":1134}
{"id":"stock","timestamp":178,"value":1705}
{"id":"stock","timestamp":186,"value":2666}
{"id":"stock","timestamp":197,"value":1666}
{"id":"stock","timestamp":202,"value":712}
{"id":"stock","timestamp":206,"value":157}
{"id":"stock","timestamp":216,"value":378}
{"id":"stock","timestamp":220,"value":-198}
{"id":"stock","timestamp":221,"value":-881}
{"id":"stock","timestamp":224,"value":-1663}
{"id":"stock","timestamp":227,"value":-1132}
{"id":"stock","timestamp":229,"value":-527}
{"id":"stock","timestamp":230,"value":467}
{"id":"stock","timestamp":231,"value":1325}
{"id":"stock","timestamp":233,"value":699}
{"id":"stock","timestamp":239,"value":851}
{"id":"stock","timestamp":242,"value":1530}
{"id":"stock","timestamp":243,"value":876}
{"id":"stock","timestamp":244,"value":1446}
{"id":"stock","timestamp":254,"value":2149}
{"id":"stock","timestamp":256,"value":3048}
{"id":"stock","timestamp":264,"value":2213}
{"id":"stock","timestamp":265,"value":1621}
{"id":"stock","timestamp":273,"value":2515}
{"id":"stock","timestamp":282,"value":1953}
{"id":"stock","timestamp":285,"value":983}
{"id":"stock","timestamp":296,"value":479}
{"id":"stock","timestamp":298,"value":1276}
{"id":"stock","timestamp":307,"value":2162}
{"id":"stock","timestamp":308,"value":1589}
{"id":"stock","timestamp":310,"value":901}
{"id":"stock","timestamp":316,"value":169}
{"id":"stock","timestamp":317,"value":1058}
{"id":"stock","timestamp":322,"value":130}
{"id":"stock","timestamp":329,"value":830}
{"id":"stock","timestamp":336,"value":1566}
{"id":"stock","timestamp":342,"value":2285}
{"id":"stock","timestamp":354,"value":1681}
{"id":"stock","timestamp":356,"value":2283}
{"id":"stock","timestamp":361,"value":3195}
{"id":"stock","timestamp":365,"value":2484}
{"id":"stock","timestamp":366,"value":1624}
{"id":"stock","timestamp":367,"value":2220}
{"id":"stock","timestamp":369,"value":1383}
{"id":"stock","timestamp":374,"value":869}
{"id":"stock","timestamp":387,"value":786}
{"id":"stock","timestamp":390,"value":-58}
{"id":"stock","timestamp":402,"value":750}
{"id":"stock","timestamp":403,"value":-2}
{"id":"stock","timestamp":410,"value":561}
{"id":"stock","timestamp":423,"value":1234}
{"id":"stock","timestamp":426,"value":254}
{"id":"stock","timestamp":436,"value":-563}
{"id":"stock","timestamp":449,"value":-1235}
{"id":"stock","timestamp":456,"value":-528}
{"id":"stock","timestamp":475,"value":-1172}
{"id":"stock","timestamp":476,"value":-605}
{"id":"stock","timestamp":480,"value":-1182}
{"id":"stock","timestamp":482,"value":-1973}
{"id":"stock","timestamp":483,"value":-975}
{"id":"stock","timestamp":489,"value":-279}
{"id":"stock","timestamp":491,"value":509}
{"id":"stock","timestamp":492,"value":1433}
{"id":"stock","timestamp":493,"value":875}
{"id":"stock","timestamp":496,"value":1496}
{"PosOutside":true,"id":"stock"}

This following specification generalizes the previous example for multiple products. It uses the delay operator to set up a timer and raise an alarm in case the stock of any product has been low for too long.

Input streams: The sales and arrivals of the three different products.

Output stream: an alarm that goes off whenever the stock of any product is too low.

time domain Double
use library Utils
use haskell Data.Maybe


#HASKELL
data Product = ProductA | ProductB | ProductC deriving (Show, Eq)
tolerance = undefined
lowval = undefined
#ENDOFHASKELL


input Int sale <Product p> 
input Int arrival <Product p> 

define Int stock <Product p>:
  ticks = ticksOf (sale p) U ticksOf (arrival p)
  val = let
    (msal, marr) = cv
    sal = 1'(fromMaybe 0) msal
    arr = 1'(fromMaybe 0) marr
    in
    stock p [<t|0] - sal + arr

define Bool low_stock <Product p> = Utils.strMap "low" (lowval p) (stock p)

define Bool cp_low_stock <Product p> = Utils.changePointsOf (low_stock p)

define TimeDiff alarm_timer <Product p>:
  ticks = ticksOf (cp_low_stock p)
  val = if cv then tolerance p else (-1)

define () alarm <Product p>:
  ticks = delay (alarm_timer p)
  val = '()

output () any_alarm:
  ticks = ticksOf (alarm ProductA) U ticksOf (alarm ProductB)
          U ticksOf (alarm ProductC)
  val = '()

-- Alternative alarm:
define TimeDiff alarm_timer2 <Product p>:
  ticks = ticksOf (cp_low_stock p) U ticksOf (arrival p)
  val = let
    (mls, marr) = cv
    ls = 1'fromJust mls
    in if (1'isJust marr) || not ls then (-1) else tolerance p
{"Time": 11, "Value": 685}
{"Time": 15, "Value": 502}
{"Time": 32, "Value": 562}
{"Time": 35, "Value": 798}
{"Time": 36, "Value": 703}
{"Time": 41, "Value": 548}
{"Time": 55, "Value": 982}
{"Time": 57, "Value": 884}
{"Time": 75, "Value": 626}
{"Time": 79, "Value": 535}
{"Time": 80, "Value": 646}
{"Time": 85, "Value": 595}
{"Time": 100, "Value": 644}
{"Time": 134, "Value": 746}
{"Time": 164, "Value": 787}
{"Time": 170, "Value": 839}
{"Time": 176, "Value": 992}
{"Time": 179, "Value": 545}
{"Time": 180, "Value": 981}
{"Time": 181, "Value": 897}
{"Time": 190, "Value": 601}
{"Time": 192, "Value": 835}
{"Time": 216, "Value": 910}
{"Time": 221, "Value": 594}
{"Time": 231, "Value": 999}
{"Time": 239, "Value": 751}
{"Time": 249, "Value": 745}
{"Time": 267, "Value": 780}
{"Time": 299, "Value": 955}
{"Time": 300, "Value": 828}
{"Time": 323, "Value": 531}
{"Time": 337, "Value": 874}
{"Time": 339, "Value": 799}
{"Time": 350, "Value": 549}
{"Time": 356, "Value": 767}
{"Time": 368, "Value": 556}
{"Time": 369, "Value": 937}
{"Time": 382, "Value": 944}
{"Time": 386, "Value": 724}
{"Time": 387, "Value": 952}
{"Time": 401, "Value": 511}
{"Time": 414, "Value": 514}
{"Time": 417, "Value": 655}
{"Time": 420, "Value": 769}
{"Time": 435, "Value": 672}
{"Time": 439, "Value": 559}
{"Time": 458, "Value": 524}
{"Time": 475, "Value": 774}
{"Time": 484, "Value": 585}
{"Time": 495, "Value": 943}
{"Time": 8, "Value": 788}
{"Time": 17, "Value": 658}
{"Time": 28, "Value": 824}
{"Time": 40, "Value": 849}
{"Time": 65, "Value": 565}
{"Time": 70, "Value": 662}
{"Time": 71, "Value": 646}
{"Time": 87, "Value": 651}
{"Time": 123, "Value": 545}
{"Time": 126, "Value": 656}
{"Time": 134, "Value": 879}
{"Time": 139, "Value": 881}
{"Time": 143, "Value": 716}
{"Time": 147, "Value": 677}
{"Time": 148, "Value": 502}
{"Time": 166, "Value": 735}
{"Time": 171, "Value": 997}
{"Time": 175, "Value": 603}
{"Time": 190, "Value": 906}
{"Time": 192, "Value": 767}
{"Time": 196, "Value": 706}
{"Time": 207, "Value": 596}
{"Time": 212, "Value": 845}
{"Time": 231, "Value": 753}
{"Time": 234, "Value": 679}
{"Time": 247, "Value": 816}
{"Time": 255, "Value": 783}
{"Time": 261, "Value": 834}
{"Time": 270, "Value": 825}
{"Time": 272, "Value": 713}
{"Time": 273, "Value": 917}
{"Time": 284, "Value": 610}
{"Time": 287, "Value": 695}
{"Time": 338, "Value": 547}
{"Time": 350, "Value": 632}
{"Time": 371, "Value": 591}
{"Time": 391, "Value": 559}
{"Time": 404, "Value": 759}
{"Time": 415, "Value": 728}
{"Time": 437, "Value": 860}
{"Time": 440, "Value": 864}
{"Time": 449, "Value": 636}
{"Time": 458, "Value": 812}
{"Time": 465, "Value": 601}
{"Time": 468, "Value": 563}
{"Time": 471, "Value": 934}
{"Time": 473, "Value": 557}
{"Time": 495, "Value": 892}
{"Time": 497, "Value": 609}
{"Time": 499, "Value": 585}
{"Time": 11, "Value": 593}
{"Time": 23, "Value": 697}
{"Time": 30, "Value": 546}
{"Time": 51, "Value": 815}
{"Time": 61, "Value": 574}
{"Time": 66, "Value": 986}
{"Time": 76, "Value": 514}
{"Time": 78, "Value": 728}
{"Time": 97, "Value": 530}
{"Time": 102, "Value": 783}
{"Time": 105, "Value": 967}
{"Time": 108, "Value": 786}
{"Time": 116, "Value": 640}
{"Time": 124, "Value": 561}
{"Time": 136, "Value": 607}
{"Time": 148, "Value": 543}
{"Time": 154, "Value": 695}
{"Time": 170, "Value": 745}
{"Time": 184, "Value": 923}
{"Time": 185, "Value": 812}
{"Time": 188, "Value": 774}
{"Time": 210, "Value": 602}
{"Time": 213, "Value": 515}
{"Time": 218, "Value": 731}
{"Time": 225, "Value": 919}
{"Time": 253, "Value": 555}
{"Time": 290, "Value": 645}
{"Time": 293, "Value": 960}
{"Time": 304, "Value": 910}
{"Time": 309, "Value": 809}
{"Time": 313, "Value": 549}
{"Time": 322, "Value": 965}
{"Time": 333, "Value": 835}
{"Time": 335, "Value": 674}
{"Time": 352, "Value": 692}
{"Time": 368, "Value": 753}
{"Time": 380, "Value": 610}
{"Time": 381, "Value": 532}
{"Time": 382, "Value": 617}
{"Time": 390, "Value": 934}
{"Time": 402, "Value": 749}
{"Time": 409, "Value": 563}
{"Time": 443, "Value": 985}
{"Time": 453, "Value": 501}
{"Time": 458, "Value": 652}
{"Time": 459, "Value": 621}
{"Time": 477, "Value": 559}
{"Time": 491, "Value": 576}
{"Time": 496, "Value": 734}
{"Time": 499, "Value": 571}
{"Time": 7, "Value": 582}
{"Time": 14, "Value": 726}
{"Time": 41, "Value": 577}
{"Time": 64, "Value": 694}
{"Time": 66, "Value": 933}
{"Time": 81, "Value": 988}
{"Time": 87, "Value": 521}
{"Time": 92, "Value": 929}
{"Time": 93, "Value": 649}
{"Time": 99, "Value": 508}
{"Time": 102, "Value": 919}
{"Time": 103, "Value": 589}
{"Time": 107, "Value": 923}
{"Time": 112, "Value": 808}
{"Time": 126, "Value": 648}
{"Time": 131, "Value": 854}
{"Time": 154, "Value": 960}
{"Time": 163, "Value": 602}
{"Time": 164, "Value": 824}
{"Time": 172, "Value": 743}
{"Time": 184, "Value": 752}
{"Time": 196, "Value": 811}
{"Time": 203, "Value": 962}
{"Time": 204, "Value": 782}
{"Time": 208, "Value": 984}
{"Time": 217, "Value": 794}
{"Time": 269, "Value": 651}
{"Time": 278, "Value": 951}
{"Time": 287, "Value": 939}
{"Time": 292, "Value": 634}
{"Time": 296, "Value": 570}
{"Time": 311, "Value": 922}
{"Time": 314, "Value": 756}
{"Time": 320, "Value": 883}
{"Time": 345, "Value": 776}
{"Time": 349, "Value": 526}
{"Time": 354, "Value": 760}
{"Time": 375, "Value": 910}
{"Time": 382, "Value": 912}
{"Time": 384, "Value": 703}
{"Time": 392, "Value": 588}
{"Time": 413, "Value": 711}
{"Time": 418, "Value": 925}
{"Time": 419, "Value": 764}
{"Time": 422, "Value": 768}
{"Time": 432, "Value": 650}
{"Time": 450, "Value": 785}
{"Time": 476, "Value": 556}
{"Time": 479, "Value": 844}
{"Time": 493, "Value": 576}
{"Time": 1, "Value": 894}
{"Time": 8, "Value": 774}
{"Time": 17, "Value": 578}
{"Time": 21, "Value": 962}
{"Time": 26, "Value": 635}
{"Time": 36, "Value": 588}
{"Time": 66, "Value": 856}
{"Time": 67, "Value": 638}
{"Time": 82, "Value": 629}
{"Time": 98, "Value": 538}
{"Time": 104, "Value": 749}
{"Time": 120, "Value": 824}
{"Time": 125, "Value": 620}
{"Time": 130, "Value": 586}
{"Time": 134, "Value": 860}
{"Time": 137, "Value": 899}
{"Time": 140, "Value": 628}
{"Time": 163, "Value": 572}
{"Time": 178, "Value": 755}
{"Time": 190, "Value": 808}
{"Time": 209, "Value": 614}
{"Time": 217, "Value": 511}
{"Time": 242, "Value": 913}
{"Time": 262, "Value": 787}
{"Time": 266, "Value": 694}
{"Time": 278, "Value": 621}
{"Time": 279, "Value": 580}
{"Time": 288, "Value": 976}
{"Time": 294, "Value": 560}
{"Time": 298, "Value": 884}
{"Time": 310, "Value": 933}
{"Time": 312, "Value": 792}
{"Time": 325, "Value": 891}
{"Time": 328, "Value": 965}
{"Time": 331, "Value": 818}
{"Time": 334, "Value": 828}
{"Time": 351, "Value": 663}
{"Time": 389, "Value": 752}
{"Time": 393, "Value": 805}
{"Time": 405, "Value": 642}
{"Time": 412, "Value": 704}
{"Time": 415, "Value": 716}
{"Time": 442, "Value": 651}
{"Time": 444, "Value": 791}
{"Time": 466, "Value": 911}
{"Time": 483, "Value": 863}
{"Time": 487, "Value": 567}
{"Time": 491, "Value": 938}
{"Time": 494, "Value": 877}
{"Time": 500, "Value": 932}
{"Time": 12, "Value": 616}
{"Time": 28, "Value": 714}
{"Time": 33, "Value": 607}
{"Time": 53, "Value": 693}
{"Time": 64, "Value": 906}
{"Time": 70, "Value": 967}
{"Time": 77, "Value": 579}
{"Time": 82, "Value": 988}
{"Time": 87, "Value": 700}
{"Time": 100, "Value": 886}
{"Time": 108, "Value": 574}
{"Time": 119, "Value": 534}
{"Time": 120, "Value": 500}
{"Time": 137, "Value": 821}
{"Time": 138, "Value": 924}
{"Time": 153, "Value": 826}
{"Time": 156, "Value": 680}
{"Time": 161, "Value": 874}
{"Time": 190, "Value": 747}
{"Time": 196, "Value": 743}
{"Time": 202, "Value": 948}
{"Time": 214, "Value": 648}
{"Time": 216, "Value": 955}
{"Time": 243, "Value": 957}
{"Time": 262, "Value": 670}
{"Time": 279, "Value": 689}
{"Time": 312, "Value": 880}
{"Time": 339, "Value": 854}
{"Time": 344, "Value": 541}
{"Time": 361, "Value": 634}
{"Time": 370, "Value": 735}
{"Time": 378, "Value": 979}
{"Time": 379, "Value": 583}
{"Time": 396, "Value": 939}
{"Time": 409, "Value": 653}
{"Time": 417, "Value": 707}
{"Time": 423, "Value": 825}
{"Time": 434, "Value": 656}
{"Time": 437, "Value": 953}
{"Time": 440, "Value": 991}
{"Time": 441, "Value": 857}
{"Time": 445, "Value": 551}
{"Time": 447, "Value": 850}
{"Time": 449, "Value": 816}
{"Time": 450, "Value": 724}
{"Time": 454, "Value": 786}
{"Time": 461, "Value": 516}
{"Time": 477, "Value": 916}
{"Time": 482, "Value": 892}
{"Time": 484, "Value": 537}
{"id":"any_alarm","timestamp":11,"value":[]}
{"id":"any_alarm","timestamp":22,"value":[]}
{"id":"any_alarm","timestamp":24,"value":[]}
{"id":"any_alarm","timestamp":43,"value":[]}
{"id":"any_alarm","timestamp":92,"value":[]}
{"id":"any_alarm","timestamp":117,"value":[]}
{"id":"any_alarm","timestamp":148,"value":[]}
{"id":"any_alarm","timestamp":188,"value":[]}
{"id":"any_alarm","timestamp":206,"value":[]}
{"id":"any_alarm","timestamp":224,"value":[]}
{"id":"any_alarm","timestamp":253,"value":[]}
{"id":"any_alarm","timestamp":279,"value":[]}
{"id":"any_alarm","timestamp":338,"value":[]}
{"id":"any_alarm","timestamp":450,"value":[]}
{"id":"any_alarm","timestamp":493,"value":[]}
{"PosOutside":true,"id":"any_alarm"}

This example makes a heavy use of the STL library to implement STL properties for the verification of a powertrain control verification from the paper Powertrain control verification benchmark, where input signals change asynchronously.

As in the cited paper, we use input data computed from a MatLab simulation of the powertrain. This example shows how to import and use the STL operators to describe properties.

We have refrained from using let and where clauses to maintain the syntax of the original properties, which are commented in MatLab above each definition.

Input streams: The events for verification, mode and pedal

Output streams: The eight different properties to check.

time domain Double
use library STL
use library Utils

input Double verification
input Double mode
input Double pedal

const simTime = 50
const eta = 1
const taus = 10 + eta
const zeta_min = 5

-- preds(i).str = 'low'; % for the pedal input signal (<0.5)
-- preds(i).str = 'high'; % for the pedal input signal (>0.5)
-- preds(i).str = 'utr'; % u<=Ut
-- preds(i).str = 'utl'; % u>=-Ut
-- preds(i).str = 'pwr'; % mode >0.5 (power mode = 1)
-- preds(i).str = 'norm'; % mode < 0.5 (normal mode = 0)

define Bool low = Utils.strMap "<0.5" (P.<0.5) pedal
define Bool high = Utils.strMap ">0.5" (P.>0.5) pedal
define Bool utl <Double x> = Utils.strMap (">-" ++ show x) (P.>(-x)) verification
define Bool utr <Double x> = Utils.strMap ("<" ++ show x) (P.<x) verification
define Bool pwr = Utils.strMap ">0.5" (P.>0.5) mode
define Bool norm = Utils.strMap "<0.5" (P.<0.5) mode

define Bool strImplies <Stream Bool x> <Stream Bool y> = neg x `disj` y

-- Opt1:
-- Ut = 0.05;
-- phi = ['[]_(' num2str(taus) ', ' num2str(simTime) ') utl /\ utr'];

const ut1 = 0.05
output Bool opt1 = STL.always (taus, simTime) (utl ut1 `conj` utr ut1)

-- Opt2:
-- Ut = 0.02;
-- phi = ['[]_(' num2str(taus) ', ' num2str(simTime) ')(((low/\<>_(0,' ...
-- num2str(h) ')high) \/ (high/\<>_(0,' num2str(h) ')low))' ...
-- '-> []_[' num2str(eta) ', ' num2str(zeta_min) '](utr /\ utl))'];
const ut2 = 0.02
output Bool opt2 = STL.always (taus, simTime) (((low `conj` STL.eventually (0,h) high) `disj`
                                    (high `conj` STL.eventually (0,h) low)) `strImplies`
                                   STL.always (eta, zeta_min) (utl ut2 `conj` utr ut2))

-- Opt3 :
-- C = 0.05;
-- Ut = C;
-- phi = ['<>_[' num2str(simTime) ',' num2str(simTime) '] utr' ];
const ut3 = 0.05
output Bool opt3 = STL.eventually (simTime, simTime) (utr ut3)

-- Opt 4:
-- Cr = 0.1;
-- Ut = Cr;
-- phi = ['[]_(' num2str(taus) ', ' num2str(simTime) ')utr'];
const ut4 = 0.1
output Bool opt4 = STL.always (taus, simTime) (utr ut4)

-- Opt 5:
-- Cr = 0.1;
-- Ut = Cl;
-- phi = ['[]_(' num2str(taus) ', ' num2str(simTime) ')utl'];
const ut5 = 0.1
output Bool opt5 = STL.always (taus, simTime) (utl ut5)

-- Opt 6:
-- Ut = 0.02;
-- phi = ['[] ((pwr /\ <>_(0,' num2str(h), ')norm) -> (<>_('num2str(eta)', ' num2str(zeta_min) ') utl /\ utr))'];

const h = 0.02
const ut6 = 0.02
output Bool opt6 = (pwr `conj` STL.eventually (0, h) norm) `strImplies` STL.eventually (eta, zeta_min) (utl ut6 `conj` utr ut6)

-- Opt 7:
-- Ut = 0.2;
-- phi = '[] (pwr -> (utl /\ utr))';
const ut7 = 0.2
output Bool opt7 = pwr `strImplies` (utl ut7 `conj` utr ut7)

-- Opt 8:
-- Ut = 0.1;
-- phi = ['[] (((low/\<>_(0,' num2str(h) ...
-- ')high) \/ (high/\<>_(0,' num2str(h) ')low)) -> [] (utr /\ utl))'];
const ut8 = 0.1
output Bool opt8 = ((low `conj` STL.eventually (0,h) high) `disj`
        (high `conj` STL.eventually (0,h) low)) `strImplies` STL.always (0,simTime) (utl ut8 `conj` utr ut8)
...
{"Time":0.9355182452, "Value":0}
{"Time":0.9360364905, "Value":0}
{"Time":0.9365547357, "Value":0}
{"Time":0.9388742018, "Value":0}
{"Time":0.94, "Value":0}
{"Time":0.9411257982, "Value":0}
{"Time":0.9422515964, "Value":0}
{"Time":0.9433773945, "Value":0}
{"Time":0.945, "Value":0}
{"Time":0.9466226055, "Value":0}
{"Time":0.9482452109, "Value":0}
{"Time":0.95, "Value":0}
{"Time":0.9517547891, "Value":0}
{"Time":0.9535095782, "Value":0}
{"Time":0.9545156736, "Value":0}
{"Time":0.955, "Value":0}
{"Time":0.9554843264, "Value":0}
{"Time":0.9559686527, "Value":0}
{"Time":0.9585530368, "Value":0}
{"Time":0.96, "Value":0}
{"Time":0.9614469632, "Value":0}
{"Time":0.9628939264, "Value":0}
{"Time":0.9643408897, "Value":0}
{"Time":0.965, "Value":0}
{"Time":0.9656591103, "Value":0}
{"Time":0.9663182207, "Value":0}
{"Time":0.9690031773, "Value":0}
{"Time":0.97, "Value":0}
{"Time":0.9709968227, "Value":0}
{"Time":0.9719936454, "Value":0}
{"Time":0.9729904682, "Value":0}
{"Time":0.975, "Value":0}
{"Time":0.9770095318, "Value":0}
{"Time":0.9790190637, "Value":0}
{"Time":0.98, "Value":0}
{"Time":0.9809809363, "Value":0}
{"Time":0.9819618727, "Value":0}
{"Time":0.982942809, "Value":0}
{"Time":0.985, "Value":0}
{"Time":0.987057191, "Value":0}
{"Time":0.989114382, "Value":0}
{"Time":0.99, "Value":0}
{"Time":0.990885618, "Value":0}
{"Time":0.9917712359, "Value":0}
{"Time":0.9926568539, "Value":0}
{"Time":0.995, "Value":0}
{"Time":0.9973431461, "Value":0}
{"Time":0.9996862922, "Value":0}
{"Time":1, "Value":0}
{"Time":1, "Value":-0.0196274747}
...
{"Time":50, "Value":0.000009997}
...
{"Time":0.9344817548, "Value":1}
{"Time":0.935, "Value":1}
{"Time":0.9355182452, "Value":1}
{"Time":0.9360364905, "Value":1}
{"Time":0.9365547357, "Value":1}
{"Time":0.9388742018, "Value":1}
{"Time":0.94, "Value":1}
{"Time":0.9411257982, "Value":1}
{"Time":0.9422515964, "Value":1}
{"Time":0.9433773945, "Value":1}
{"Time":0.945, "Value":1}
{"Time":0.9466226055, "Value":1}
{"Time":0.9482452109, "Value":1}
{"Time":0.95, "Value":1}
{"Time":0.9517547891, "Value":1}
{"Time":0.9535095782, "Value":1}
{"Time":0.9545156736, "Value":1}
{"Time":0.955, "Value":1}
{"Time":0.9554843264, "Value":1}
{"Time":0.9559686527, "Value":1}
{"Time":0.9585530368, "Value":1}
{"Time":0.96, "Value":1}
{"Time":0.9614469632, "Value":1}
{"Time":0.9628939264, "Value":1}
{"Time":0.9643408897, "Value":1}
{"Time":0.965, "Value":1}
{"Time":0.9656591103, "Value":1}
{"Time":0.9663182207, "Value":1}
{"Time":0.9690031773, "Value":1}
{"Time":0.97, "Value":1}
{"Time":0.9709968227, "Value":1}
{"Time":0.9719936454, "Value":1}
{"Time":0.9729904682, "Value":1}
{"Time":0.975, "Value":1}
{"Time":0.9770095318, "Value":1}
{"Time":0.9790190637, "Value":1}
{"Time":0.98, "Value":1}
{"Time":0.9809809363, "Value":1}
{"Time":0.9819618727, "Value":1}
{"Time":0.982942809, "Value":1}
{"Time":0.985, "Value":1}
{"Time":0.987057191, "Value":1}
{"Time":0.989114382, "Value":1}
{"Time":0.99, "Value":1}
{"Time":0.990885618, "Value":1}
{"Time":0.9917712359, "Value":1}
{"Time":0.9926568539, "Value":1}
{"Time":0.995, "Value":1}
{"Time":0.9973431461, "Value":1}
{"Time":0.9996862922, "Value":1}
{"Time":1, "Value":1}
...
{"Time":50, "Value":1}
...
{"Time":0.9355182452, "Value": 0}
{"Time":0.9360364905, "Value": 0}
{"Time":0.9365547357, "Value": 0}
{"Time":0.9388742018, "Value": 0}
{"Time":0.94, "Value": 0}
{"Time":0.9411257982, "Value": 0}
{"Time":0.9422515964, "Value": 0}
{"Time":0.9433773945, "Value": 0}
{"Time":0.945, "Value": 0}
{"Time":0.9466226055, "Value": 0}
{"Time":0.9482452109, "Value": 0}
{"Time":0.95, "Value": 0}
{"Time":0.9517547891, "Value": 0}
{"Time":0.9535095782, "Value": 0}
{"Time":0.9545156736, "Value": 0}
{"Time":0.955, "Value": 0}
{"Time":0.9554843264, "Value": 0}
{"Time":0.9559686527, "Value": 0}
{"Time":0.9585530368, "Value": 0}
{"Time":0.96, "Value": 0}
{"Time":0.9614469632, "Value": 0}
{"Time":0.9628939264, "Value": 0}
{"Time":0.9643408897, "Value": 0}
{"Time":0.965, "Value": 0}
{"Time":0.9656591103, "Value": 0}
{"Time":0.9663182207, "Value": 0}
{"Time":0.9690031773, "Value": 0}
{"Time":0.97, "Value": 0}
{"Time":0.9709968227, "Value": 0}
{"Time":0.9719936454, "Value": 0}
{"Time":0.9729904682, "Value": 0}
{"Time":0.975, "Value": 0}
{"Time":0.9770095318, "Value": 0}
{"Time":0.9790190637, "Value": 0}
{"Time":0.98, "Value": 0}
{"Time":0.9809809363, "Value": 0}
{"Time":0.9819618727, "Value": 0}
{"Time":0.982942809, "Value": 0}
{"Time":0.985, "Value": 0}
{"Time":0.987057191, "Value": 0}
{"Time":0.989114382, "Value": 0}
{"Time":0.99, "Value": 0}
{"Time":0.990885618, "Value": 0}
{"Time":0.9917712359, "Value": 0}
{"Time":0.9926568539, "Value": 0}
{"Time":0.995, "Value": 0}
{"Time":0.9973431461, "Value": 0}
{"Time":0.9996862922, "Value": 0}
{"Time":1, "Value": 0}
{"Time":1, "Value": 0}
...
{"Time":50, "Value": 0}
...
{"id":"opt6","timestamp":8.999999999999986e-2,"value":true}
{"id":"opt7","timestamp":9.0e-2,"value":true}
{"id":"opt8","timestamp":9.0e-2,"value":true}
{"id":"opt6","timestamp":9.0e-2,"value":true}
{"id":"opt8","timestamp":9.0673675e-2,"value":true}
{"id":"opt7","timestamp":9.08706135e-2,"value":true}
{"id":"opt8","timestamp":9.08706135e-2,"value":true}
{"id":"opt6","timestamp":9.08706135e-2,"value":true}
{"id":"opt8","timestamp":9.13473499e-2,"value":true}
{"id":"opt7","timestamp":9.17412271e-2,"value":true}
{"id":"opt8","timestamp":9.17412271e-2,"value":true}
{"id":"opt6","timestamp":9.17412271e-2,"value":true}
{"id":"opt8","timestamp":9.20210249e-2,"value":true}
{"id":"opt6","timestamp":9.240560850000001e-2,"value":true}
{"id":"opt7","timestamp":9.26118406e-2,"value":true}
{"id":"opt8","timestamp":9.26118406e-2,"value":true}
{"id":"opt6","timestamp":9.26118406e-2,"value":true}
{"id":"opt6","timestamp":9.499999999999975e-2,"value":true}
{"id":"opt7","timestamp":9.5e-2,"value":true}
{"id":"opt8","timestamp":9.5e-2,"value":true}
{"id":"opt6","timestamp":9.5e-2,"value":true}
{"id":"opt7","timestamp":9.73881594e-2,"value":true}
{"id":"opt8","timestamp":9.73881594e-2,"value":true}
{"id":"opt6","timestamp":9.73881594e-2,"value":true}
{"id":"opt6","timestamp":9.759439150000038e-2,"value":true}
{"id":"opt8","timestamp":9.797897509999999e-2,"value":true}
{"id":"opt6","timestamp":9.999999999999964e-2,"value":true}
{"id":"opt8","timestamp":9.999999999999999e-2,"value":true}
{"id":"opt7","timestamp":0.1,"value":true}
{"id":"opt8","timestamp":0.1,"value":true}
{"id":"opt6","timestamp":0.1,"value":true}
{"id":"opt7","timestamp":0.1009456125,"value":true}
{"id":"opt8","timestamp":0.1009456125,"value":true}
{"id":"opt6","timestamp":0.1009456125,"value":true}
{"id":"opt8","timestamp":0.1011068633,"value":true}
{"id":"opt7","timestamp":0.101891225,"value":true}
{"id":"opt8","timestamp":0.101891225,"value":true}
{"id":"opt6","timestamp":0.101891225,"value":true}
{"id":"opt8","timestamp":0.10221372649999999,"value":true}
{"id":"opt6","timestamp":0.1024056084999998,"value":true}
{"id":"opt7","timestamp":0.1028368375,"value":true}
{"id":"opt8","timestamp":0.1028368375,"value":true}
{"id":"opt6","timestamp":0.1028368375,"value":true}
{"id":"opt8","timestamp":0.1033205898,"value":true}
{"id":"opt7","timestamp":0.105,"value":true}
{"id":"opt8","timestamp":0.105,"value":true}
{"id":"opt6","timestamp":0.105,"value":true}
{"id":"opt6","timestamp":0.10500000000000043,"value":true}
{"id":"opt8","timestamp":0.1066794102,"value":true}
{"id":"opt7","timestamp":0.1071631625,"value":true}
{"id":"opt8","timestamp":0.1071631625,"value":true}
{"id":"opt6","timestamp":0.1071631625,"value":true}
{"id":"opt6","timestamp":0.10759439150000016,"value":true}
{"id":"opt8","timestamp":0.10835882039999999,"value":true}
{"id":"opt7","timestamp":0.109326325,"value":true}
{"id":"opt8","timestamp":0.109326325,"value":true}
{"id":"opt6","timestamp":0.109326325,"value":true}
{"id":"opt7","timestamp":0.11,"value":true}
{"id":"opt8","timestamp":0.11,"value":true}
{"id":"opt6","timestamp":0.11,"value":true}
{"id":"opt6","timestamp":0.11000000000000032,"value":true}
{"id":"opt7","timestamp":0.110673675,"value":true}
{"id":"opt8","timestamp":0.110673675,"value":true}
{"id":"opt6","timestamp":0.110673675,"value":true}
{"id":"opt8","timestamp":0.11119656509999999,"value":true}
{"id":"opt7","timestamp":0.1113473499,"value":true}
{"id":"opt8","timestamp":0.1113473499,"value":true}
{"id":"opt6","timestamp":0.1113473499,"value":true}
{"id":"opt7","timestamp":0.1120210249,"value":true}
{"id":"opt8","timestamp":0.1120210249,"value":true}
{"id":"opt6","timestamp":0.1120210249,"value":true}
{"id":"opt8","timestamp":0.1123931301,"value":true}
{"id":"opt6","timestamp":0.11240560849999959,"value":true}
{"id":"opt8","timestamp":0.1135896952,"value":true}
{"id":"opt7","timestamp":0.115,"value":true}
{"id":"opt8","timestamp":0.115,"value":true}
{"id":"opt6","timestamp":0.115,"value":true}
{"id":"opt6","timestamp":0.11500000000000021,"value":true}
{"id":"opt8","timestamp":0.11641030479999999,"value":true}
{"id":"opt6","timestamp":0.11759439149999995,"value":true}
{"id":"opt8","timestamp":0.11782060970000001,"value":true}
{"id":"opt7","timestamp":0.1179789751,"value":true}
{"id":"opt8","timestamp":0.1179789751,"value":true}
{"id":"opt6","timestamp":0.1179789751,"value":true}
{"id":"opt8","timestamp":0.1192309145,"value":true}
{"id":"opt7","timestamp":0.12,"value":true}
{"id":"opt8","timestamp":0.12,"value":true}
{"id":"opt6","timestamp":0.12,"value":true}
{"id":"opt8","timestamp":0.12000000000000001,"value":true}
{"id":"opt6","timestamp":0.1200000000000001,"value":true}
{"id":"opt8","timestamp":0.1207690855,"value":true}
{"id":"opt7","timestamp":0.1211068633,"value":true}
{"id":"opt8","timestamp":0.1211068633,"value":true}
{"id":"opt6","timestamp":0.1211068633,"value":true}
{"id":"opt8","timestamp":0.1215381709,"value":true}
{"id":"opt7","timestamp":0.1222137265,"value":true}
{"id":"opt8","timestamp":0.1222137265,"value":true}
{"id":"opt6","timestamp":0.1222137265,"value":true}
{"id":"opt8","timestamp":0.1223072564,"value":true}
{"id":"opt6","timestamp":0.12240560850000026,"value":true}
{"id":"opt7","timestamp":0.1233205898,"value":true}
{"id":"opt8","timestamp":0.1233205898,"value":true}
{"id":"opt6","timestamp":0.1233205898,"value":true}
{"id":"opt8","timestamp":0.12499999999999999,"value":true}
{"id":"opt7","timestamp":0.125,"value":true}
{"id":"opt8","timestamp":0.125,"value":true}
{"id":"opt6","timestamp":0.125,"value":true}
{"id":"opt7","timestamp":0.1266794102,"value":true}
{"id":"opt8","timestamp":0.1266794102,"value":true}
{"id":"opt6","timestamp":0.1266794102,"value":true}
{"id":"opt6","timestamp":0.12759439149999974,"value":true}
{"id":"opt8","timestamp":0.12769274360000002,"value":true}
{"id":"opt7","timestamp":0.1283588204,"value":true}
{"id":"opt8","timestamp":0.1283588204,"value":true}
{"id":"opt6","timestamp":0.1283588204,"value":true}
{"id":"opt6","timestamp":0.1299999999999999,"value":true}
{"id":"opt7","timestamp":0.13,"value":true}
{"id":"opt8","timestamp":0.13,"value":true}
{"id":"opt6","timestamp":0.13,"value":true}
{"id":"opt7","timestamp":0.1311965651,"value":true}
{"id":"opt8","timestamp":0.1311965651,"value":true}
{"id":"opt6","timestamp":0.1311965651,"value":true}
{"id":"opt8","timestamp":0.1313810927,"value":true}
{"id":"opt7","timestamp":0.1323931301,"value":true}
{"id":"opt8","timestamp":0.1323931301,"value":true}
{"id":"opt6","timestamp":0.1323931301,"value":true}
{"id":"opt6","timestamp":0.13240560850000005,"value":true}
{"id":"opt8","timestamp":0.1327621854,"value":true}
{"id":"opt7","timestamp":0.1335896952,"value":true}
{"id":"opt8","timestamp":0.1335896952,"value":true}
{"id":"opt6","timestamp":0.1335896952,"value":true}
{"id":"opt8","timestamp":0.1341432781,"value":true}
{"id":"opt6","timestamp":0.1349999999999998,"value":true}
{"id":"opt7","timestamp":0.135,"value":true}
{"id":"opt8","timestamp":0.135,"value":true}
{"id":"opt6","timestamp":0.135,"value":true}
{"id":"opt8","timestamp":0.1358567219,"value":true}
{"id":"opt7","timestamp":0.1364103048,"value":true}
{"id":"opt8","timestamp":0.1364103048,"value":true}
{"id":"opt6","timestamp":0.1364103048,"value":true}
{"id":"opt8","timestamp":0.1367134438,"value":true}
{"id":"opt8","timestamp":0.1375701658,"value":true}
{"id":"opt6","timestamp":0.1375943915000004,"value":true}
{"id":"opt7","timestamp":0.1378206097,"value":true}
{"id":"opt8","timestamp":0.1378206097,"value":true}
{"id":"opt6","timestamp":0.1378206097,"value":true}
{"id":"opt7","timestamp":0.1392309145,"value":true}
{"id":"opt8","timestamp":0.1392309145,"value":true}
{"id":"opt6","timestamp":0.1392309145,"value":true}
{"id":"opt6","timestamp":0.13999999999999968,"value":true}
{"id":"opt7","timestamp":0.14,"value":true}
{"id":"opt8","timestamp":0.14,"value":true}
{"id":"opt6","timestamp":0.14,"value":true}
{"id":"opt7","timestamp":0.1407690855,"value":true}
{"id":"opt8","timestamp":0.1407690855,"value":true}
{"id":"opt6","timestamp":0.1407690855,"value":true}
{"id":"opt8","timestamp":0.14148239750000002,"value":true}
{"id":"opt7","timestamp":0.1415381709,"value":true}
{"id":"opt8","timestamp":0.1415381709,"value":true}
{"id":"opt6","timestamp":0.1415381709,"value":true}
{"id":"opt7","timestamp":0.1423072564,"value":true}
{"id":"opt8","timestamp":0.1423072564,"value":true}
{"id":"opt6","timestamp":0.1423072564,"value":true}
{"id":"opt6","timestamp":0.14240560849999984,"value":true}
{"id":"opt8","timestamp":0.142964795,"value":true}
{"id":"opt8","timestamp":0.14444719250000002,"value":true}
{"id":"opt6","timestamp":0.14499999999999957,"value":true}
{"id":"opt7","timestamp":0.145,"value":true}
{"id":"opt8","timestamp":0.145,"value":true}
{"id":"opt6","timestamp":0.145,"value":true}
{"id":"opt8","timestamp":0.14500000000000002,"value":true}
{"id":"opt8","timestamp":0.14555280750000002,"value":true}
{"id":"opt8","timestamp":0.14610561500000002,"value":true}
{"id":"opt8","timestamp":0.1466584225,"value":true}
{"id":"opt6","timestamp":0.1475943915000002,"value":true}
{"id":"opt7","timestamp":0.1476927436,"value":true}
{"id":"opt8","timestamp":0.1476927436,"value":true}
{"id":"opt6","timestamp":0.1476927436,"value":true}
{"id":"opt8","timestamp":0.14959891790000002,"value":true}
{"id":"opt7","timestamp":0.15,"value":true}
{"id":"opt8","timestamp":0.15,"value":true}
{"id":"opt6","timestamp":0.15,"value":true}
{"id":"opt8","timestamp":0.15000000000000002,"value":true}
{"id":"opt6","timestamp":0.15000000000000036,"value":true}
{"id":"opt8","timestamp":0.1504010821,"value":true}
{"id":"opt8","timestamp":0.1508021643,"value":true}
{"id":"opt8","timestamp":0.15120324640000002,"value":true}
{"id":"opt7","timestamp":0.1513810927,"value":true}
{"id":"opt8","timestamp":0.1513810927,"value":true}
{"id":"opt6","timestamp":0.1513810927,"value":true}
{"id":"opt6","timestamp":0.15240560849999962,"value":true}
{"id":"opt7","timestamp":0.1527621854,"value":true}
{"id":"opt8","timestamp":0.1527621854,"value":true}
{"id":"opt6","timestamp":0.1527621854,"value":true}
{"id":"opt7","timestamp":0.1541432781,"value":true}
{"id":"opt8","timestamp":0.1541432781,"value":true}
{"id":"opt6","timestamp":0.1541432781,"value":true}
{"id":"opt8","timestamp":0.15451041670000001,"value":true}
{"id":"opt7","timestamp":0.155,"value":true}
{"id":"opt8","timestamp":0.155,"value":true}
{"id":"opt6","timestamp":0.155,"value":true}
{"id":"opt6","timestamp":0.15500000000000025,"value":true}
{"id":"opt8","timestamp":0.1554895833,"value":true}
{"id":"opt7","timestamp":0.1558567219,"value":true}
{"id":"opt8","timestamp":0.1558567219,"value":true}
{"id":"opt6","timestamp":0.1558567219,"value":true}
{"id":"opt8","timestamp":0.1559791667,"value":true}
{"id":"opt8","timestamp":0.15646875000000002,"value":true}
{"id":"opt7","timestamp":0.1567134438,"value":true}
{"id":"opt8","timestamp":0.1567134438,"value":true}
{"id":"opt6","timestamp":0.1567134438,"value":true}
{"id":"opt7","timestamp":0.1575701658,"value":true}
{"id":"opt8","timestamp":0.1575701658,"value":true}
{"id":"opt6","timestamp":0.1575701658,"value":true}
{"id":"opt6","timestamp":0.1575943915,"value":true}
{"id":"opt7","timestamp":0.16,"value":true}
{"id":"opt8","timestamp":0.16,"value":true}
{"id":"opt6","timestamp":0.16,"value":true}
{"id":"opt6","timestamp":0.16000000000000014,"value":true}
{"id":"opt7","timestamp":0.1614823975,"value":true}
{"id":"opt8","timestamp":0.1614823975,"value":true}
{"id":"opt6","timestamp":0.1614823975,"value":true}
{"id":"opt8","timestamp":0.16169612630000002,"value":true}
{"id":"opt6","timestamp":0.1624056085000003,"value":true}
{"id":"opt7","timestamp":0.162964795,"value":true}
{"id":"opt8","timestamp":0.162964795,"value":true}
{"id":"opt6","timestamp":0.162964795,"value":true}
{"id":"opt8","timestamp":0.1633922526,"value":true}
{"id":"opt7","timestamp":0.1644471925,"value":true}
{"id":"opt8","timestamp":0.1644471925,"value":true}
{"id":"opt6","timestamp":0.1644471925,"value":true}
{"id":"opt7","timestamp":0.165,"value":true}
{"id":"opt8","timestamp":0.165,"value":true}
{"id":"opt6","timestamp":0.165,"value":true}
{"id":"opt6","timestamp":0.16500000000000004,"value":true}
{"id":"opt7","timestamp":0.1655528075,"value":true}
{"id":"opt8","timestamp":0.1655528075,"value":true}
{"id":"opt6","timestamp":0.1655528075,"value":true}
{"id":"opt7","timestamp":0.166105615,"value":true}
{"id":"opt8","timestamp":0.166105615,"value":true}
{"id":"opt6","timestamp":0.166105615,"value":true}
{"id":"opt8","timestamp":0.1666077474,"value":true}
{"id":"opt7","timestamp":0.1666584225,"value":true}
{"id":"opt8","timestamp":0.1666584225,"value":true}
{"id":"opt6","timestamp":0.1666584225,"value":true}
{"id":"opt6","timestamp":0.16759439149999977,"value":true}
{"id":"opt8","timestamp":0.1682154948,"value":true}
{"id":"opt7","timestamp":0.1695989179,"value":true}
{"id":"opt8","timestamp":0.1695989179,"value":true}
{"id":"opt6","timestamp":0.1695989179,"value":true}
{"id":"opt6","timestamp":0.16999999999999993,"value":true}
{"id":"opt7","timestamp":0.17,"value":true}
{"id":"opt8","timestamp":0.17,"value":true}
{"id":"opt6","timestamp":0.17,"value":true}
{"id":"opt7","timestamp":0.1704010821,"value":true}
{"id":"opt8","timestamp":0.1704010821,"value":true}
{"id":"opt6","timestamp":0.1704010821,"value":true}
{"id":"opt7","timestamp":0.1708021643,"value":true}
{"id":"opt8","timestamp":0.1708021643,"value":true}
{"id":"opt6","timestamp":0.1708021643,"value":true}
{"id":"opt7","timestamp":0.1712032464,"value":true}
{"id":"opt8","timestamp":0.1712032464,"value":true}
{"id":"opt6","timestamp":0.1712032464,"value":true}
{"id":"opt8","timestamp":0.17178450520000002,"value":true}
{"id":"opt6","timestamp":0.17240560850000008,"value":true}
{"id":"opt8","timestamp":0.1735690105,"value":true}
{"id":"opt7","timestamp":0.1745104167,"value":true}
{"id":"opt8","timestamp":0.1745104167,"value":true}
{"id":"opt6","timestamp":0.1745104167,"value":true}
{"id":"opt6","timestamp":0.17499999999999982,"value":true}
{"id":"opt7","timestamp":0.175,"value":true}
{"id":"opt8","timestamp":0.175,"value":true}
{"id":"opt6","timestamp":0.175,"value":true}
{"id":"opt8","timestamp":0.17500000000000002,"value":true}
{"id":"opt7","timestamp":0.1754895833,"value":true}
{"id":"opt8","timestamp":0.1754895833,"value":true}
{"id":"opt6","timestamp":0.1754895833,"value":true}
{"id":"opt7","timestamp":0.1759791667,"value":true}
{"id":"opt8","timestamp":0.1759791667,"value":true}
{"id":"opt6","timestamp":0.1759791667,"value":true}
{"id":"opt8","timestamp":0.1764309895,"value":true}
{"id":"opt7","timestamp":0.17646875,"value":true}
{"id":"opt8","timestamp":0.17646875,"value":true}
{"id":"opt6","timestamp":0.17646875,"value":true}
{"id":"opt6","timestamp":0.17759439149999956,"value":true}
{"id":"opt8","timestamp":0.177861979,"value":true}
{"id":"opt6","timestamp":0.17999999999999972,"value":true}
{"id":"opt7","timestamp":0.18,"value":true}
{"id":"opt8","timestamp":0.18,"value":true}
{"id":"opt6","timestamp":0.18,"value":true}
{"id":"opt8","timestamp":0.18000000000000002,"value":true}
{"id":"opt7","timestamp":0.1816961263,"value":true}
{"id":"opt8","timestamp":0.1816961263,"value":true}
{"id":"opt6","timestamp":0.1816961263,"value":true}
{"id":"opt8","timestamp":0.1820853909,"value":true}
{"id":"opt6","timestamp":0.18240560849999987,"value":true}
{"id":"opt7","timestamp":0.1833922526,"value":true}
{"id":"opt8","timestamp":0.1833922526,"value":true}
{"id":"opt6","timestamp":0.1833922526,"value":true}
...
{"id":"opt6","timestamp":49.995,"value":true}
{"id":"opt7","timestamp":49.9975452393,"value":true}
{"id":"opt8","timestamp":49.9975452393,"value":true}
{"id":"opt6","timestamp":49.9975452393,"value":true}
{"id":"opt7","timestamp":50,"value":true}
{"id":"opt8","timestamp":50,"value":true}
{"id":"opt6","timestamp":50,"value":true}
{"PosOutside":true,"id":"opt3"}
{"PosOutside":true,"id":"opt4"}
{"PosOutside":true,"id":"opt1"}
{"PosOutside":true,"id":"opt5"}
{"PosOutside":true,"id":"opt2"}
{"PosOutside":true,"id":"opt7"}
{"PosOutside":true,"id":"opt8"}
{"PosOutside":true,"id":"opt6"}

This example illustrates a simple STL specification: if the input speed becomes toofast, then speed will decelerate continuously until reaching an admissible speed speedok within 0.5 time units (represented by the stream slow_down).

This example shows a straightforward use of the STL library to define temporal properties as streams.

Input stream: The speed of the vehicle.

Output stream: An indicator that the property is preserved.

time domain Double

use library STL
use library Utils

const max_speed = 5
const ok_speed = 4

input Double speed

define Bool toofast = Utils.strMap "toofast" (P.>max_speed) speed

define Bool speedok = Utils.strMap "speedok" (P.<=ok_speed) speed

define Bool decel:
  ticks = ticksOf speed
  val = cv > speed[t>|0]

define Bool slow_down = STL.until (0,5) decel speedok

output Bool ok:
  ticks = ticksOf toofast U ticksOf slow_down
  val = toofast [~t|False] `implies` slow_down [~t|True]
{"Time": 2, "Value": 2}
{"Time": 29, "Value": 4}
{"Time": 33, "Value": 5}
{"Time": 37, "Value": 3}
{"Time": 42, "Value": 5}
{"Time": 73, "Value": 2}
{"Time": 82, "Value": 2}
{"Time": 96, "Value": 2}
{"Time": 104, "Value": 5}
{"Time": 112, "Value": 6}
{"Time": 119, "Value": 2}
{"Time": 120, "Value": 5}
{"Time": 127, "Value": 7}
{"Time": 131, "Value": 5}
{"Time": 139, "Value": 3}
{"Time": 155, "Value": 2}
{"Time": 158, "Value": 3}
{"Time": 174, "Value": 7}
{"Time": 176, "Value": 4}
{"Time": 180, "Value": 3}
{"Time": 183, "Value": 2}
{"Time": 198, "Value": 2}
{"Time": 199, "Value": 6}
{"Time": 222, "Value": 4}
{"Time": 229, "Value": 6}
{"Time": 236, "Value": 4}
{"Time": 237, "Value": 2}
{"Time": 244, "Value": 3}
{"Time": 253, "Value": 3}
{"Time": 257, "Value": 5}
{"Time": 291, "Value": 2}
{"Time": 295, "Value": 3}
{"Time": 305, "Value": 7}
{"Time": 329, "Value": 4}
{"Time": 333, "Value": 2}
{"Time": 334, "Value": 6}
{"Time": 337, "Value": 2}
{"Time": 360, "Value": 7}
{"Time": 383, "Value": 5}
{"Time": 401, "Value": 3}
{"Time": 402, "Value": 3}
{"Time": 405, "Value": 7}
{"Time": 419, "Value": 3}
{"Time": 427, "Value": 7}
{"Time": 430, "Value": 2}
{"Time": 440, "Value": 6}
{"Time": 442, "Value": 7}
{"Time": 451, "Value": 3}
{"Time": 460, "Value": 3}
{"Time": 467, "Value": 3}
{"id":"ok","timestamp":-3,"value":true}
{"id":"ok","timestamp":2,"value":true}
{"id":"ok","timestamp":24,"value":true}
{"id":"ok","timestamp":28,"value":true}
{"id":"ok","timestamp":29,"value":true}
{"id":"ok","timestamp":32,"value":true}
{"id":"ok","timestamp":33,"value":true}
{"id":"ok","timestamp":37,"value":true}
{"id":"ok","timestamp":42,"value":true}
{"id":"ok","timestamp":68,"value":true}
{"id":"ok","timestamp":73,"value":true}
{"id":"ok","timestamp":77,"value":true}
{"id":"ok","timestamp":82,"value":true}
{"id":"ok","timestamp":91,"value":true}
{"id":"ok","timestamp":96,"value":true}
{"id":"ok","timestamp":99,"value":true}
{"id":"ok","timestamp":104,"value":true}
{"id":"ok","timestamp":107,"value":true}
{"id":"ok","timestamp":112,"value":false}
{"id":"ok","timestamp":114,"value":true}
{"id":"ok","timestamp":115,"value":true}
{"id":"ok","timestamp":119,"value":true}
{"id":"ok","timestamp":120,"value":true}
{"id":"ok","timestamp":122,"value":true}
{"id":"ok","timestamp":126,"value":true}
{"id":"ok","timestamp":127,"value":false}
{"id":"ok","timestamp":131,"value":true}
{"id":"ok","timestamp":134,"value":true}
{"id":"ok","timestamp":139,"value":true}
{"id":"ok","timestamp":150,"value":true}
{"id":"ok","timestamp":153,"value":true}
{"id":"ok","timestamp":155,"value":true}
{"id":"ok","timestamp":158,"value":true}
{"id":"ok","timestamp":169,"value":true}
{"id":"ok","timestamp":171,"value":true}
{"id":"ok","timestamp":174,"value":true}
{"id":"ok","timestamp":175,"value":true}
{"id":"ok","timestamp":176,"value":true}
{"id":"ok","timestamp":178,"value":true}
{"id":"ok","timestamp":180,"value":true}
{"id":"ok","timestamp":183,"value":true}
{"id":"ok","timestamp":193,"value":true}
{"id":"ok","timestamp":194,"value":true}
{"id":"ok","timestamp":198,"value":true}
{"id":"ok","timestamp":199,"value":false}
{"id":"ok","timestamp":217,"value":true}
{"id":"ok","timestamp":222,"value":true}
{"id":"ok","timestamp":224,"value":true}
{"id":"ok","timestamp":229,"value":false}
{"id":"ok","timestamp":231,"value":true}
{"id":"ok","timestamp":232,"value":true}
{"id":"ok","timestamp":236,"value":true}
{"id":"ok","timestamp":237,"value":true}
{"id":"ok","timestamp":239,"value":true}
{"id":"ok","timestamp":244,"value":true}
{"id":"ok","timestamp":248,"value":true}
{"id":"ok","timestamp":252,"value":true}
{"id":"ok","timestamp":253,"value":true}
{"id":"ok","timestamp":257,"value":true}
{"id":"ok","timestamp":286,"value":true}
{"id":"ok","timestamp":290,"value":true}
{"id":"ok","timestamp":291,"value":true}
{"id":"ok","timestamp":295,"value":true}
{"id":"ok","timestamp":300,"value":true}
{"id":"ok","timestamp":305,"value":false}
{"id":"ok","timestamp":324,"value":true}
{"id":"ok","timestamp":328,"value":true}
{"id":"ok","timestamp":329,"value":true}
{"id":"ok","timestamp":332,"value":true}
{"id":"ok","timestamp":333,"value":true}
{"id":"ok","timestamp":334,"value":true}
{"id":"ok","timestamp":337,"value":true}
{"id":"ok","timestamp":355,"value":true}
{"id":"ok","timestamp":360,"value":false}
{"id":"ok","timestamp":378,"value":false}
{"id":"ok","timestamp":383,"value":true}
{"id":"ok","timestamp":396,"value":true}
{"id":"ok","timestamp":397,"value":true}
{"id":"ok","timestamp":400,"value":true}
{"id":"ok","timestamp":401,"value":true}
{"id":"ok","timestamp":402,"value":true}
{"id":"ok","timestamp":405,"value":false}
{"id":"ok","timestamp":414,"value":true}
{"id":"ok","timestamp":419,"value":true}
{"id":"ok","timestamp":422,"value":true}
{"id":"ok","timestamp":425,"value":true}
{"id":"ok","timestamp":427,"value":true}
{"id":"ok","timestamp":430,"value":true}
{"id":"ok","timestamp":435,"value":true}
{"id":"ok","timestamp":437,"value":true}
{"id":"ok","timestamp":440,"value":false}
{"id":"ok","timestamp":442,"value":false}
{"id":"ok","timestamp":446,"value":true}
{"id":"ok","timestamp":451,"value":true}
{"id":"ok","timestamp":455,"value":true}
{"id":"ok","timestamp":460,"value":true}
{"id":"ok","timestamp":462,"value":true}
{"id":"ok","timestamp":467,"value":true}
{"PosOutside":true,"id":"ok"}
This example is a smart home specification that uses A Dataset of Routine Daily Activities in an Instrumented Home .

The following monitor calculates how much time residents spend watching TV per day, assessing that every day the people living the house should not watch more than three hours of TV exceeded3hPerDay.

More interesting is exceededAvgPlus30m, which states that residents should not watch thirty minutes more than the total average of TV watched historically.

This threshold is dynamic, and requires declaring intermediate quantitative streams that compute the average and current day TV time.

Input streams: TV status of the living room and the office

Output streams: exceeded3hPerDay and exceededAvgPlus30m

time domain UTC

use library Utils
use haskell Data.Time


#HASKELL
data TVStatus = OFF | ON deriving (Show,Generic,Read,FromJSON,ToJSON,Eq)
#ENDOFHASKELL


const instantsPerMinute = 1

input TVStatus livingroom_tv_status
input TVStatus office_tv_status

define Bool livingroom_tv_on = Utils.strMap "isOn" (==ON) livingroom_tv_status
define Bool office_tv_on = Utils.strMap "isOn" (==ON) office_tv_status

define Bool any_tv_on:
  ticks = ticksOf office_tv_on U ticksOf livingroom_tv_on
  val = office_tv_on [~t|False] || livingroom_tv_on [~t|False]

define Int instantN:
  ticks = ticksOf any_tv_on
  val = instantN [<t|0] + 1

define Bool isNewDay:
  ticks = ticksOf any_tv_on
  val = let
    today = 1'utctDay now
    prev = 1'(utctDay.unT) (timeOf (any_tv_on << t))
    in
    if instantN [~t|] === 1 then 'True else today /== prev

define Int howMuchTvToday:
  ticks = ticksOf any_tv_on
  val = let
    prevVal = if isNewDay [~t|] then 0 else howMuchTvToday [<t|0]
    sumVal = if any_tv_on [~t|] then 1 else 0
    in
    prevVal + sumVal

output Bool exceeded3hPerDay:
  ticks = ticksOf any_tv_on
  val = howMuchTvToday[~t|] > 3*60*instantsPerMinute

define Int countDays:
  ticks = ticksOf any_tv_on
  val = countDays [<t|0] + if isNewDay[~t|] then 1 else 0

define Int totalTVTime:
  ticks = ticksOf any_tv_on
  val = totalTVTime [<t|0] + if any_tv_on[~t|] then 1 else 0

define Int avgTvPast:
  ticks = ticksOf any_tv_on
  val = if isNewDay[~t|] then 2'div (totalTVTime[~t|]) (countDays[~t|]) else avgTvPast [<t|0]

output Bool exceededAvgPlus30m:
  ticks = ticksOf any_tv_on
  val = howMuchTvToday[~t|] > avgTvPast[~t|] + 30 * instantsPerMinute
{"Value": "OFF", "Time": {"hour": 7, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 24}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 25}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 26}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 27}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 28}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 29}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 30}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 31}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 32}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 33}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 34}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 35}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 36}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 37}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 38}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 39}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 40}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 41}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 42}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 43}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 44}}
{"Value": "ON", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 45}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 46}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 47}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 48}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 49}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 0.0, "year": 2017, "day": 30, "minute": 50}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 1.0, "year": 2017, "day": 30, "minute": 51}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 52}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 53}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 54}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 55}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 56}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 57}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 58}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 38}}
...
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 38}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 39}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 40}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 41}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 42}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 43}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 44}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 45}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 46}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 47}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 48}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 49}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 50}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 51}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 52}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 53}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 54}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 55}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 56}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 57}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 58}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 38}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 39}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 40}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 41}}
{"Value": "OFF", "Time": {"hour": 7, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 38}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 39}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 40}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 41}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 42}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 43}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 44}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 45}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 46}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 47}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 48}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 49}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 50}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 51}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 52}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 53}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 54}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 55}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 56}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 57}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 58}}
{"Value": "OFF", "Time": {"hour": 8, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 9, "month": 0, "second": 2.0, "year": 2017, "day": 30, "minute": 38}}
...
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 38}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 39}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 40}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 41}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 42}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 43}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 44}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 45}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 46}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 47}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 48}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 49}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 50}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 51}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 52}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 53}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 54}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 55}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 56}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 57}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 58}}
{"Value": "OFF", "Time": {"hour": 15, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 59}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 0}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 1}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 2}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 3}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 4}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 5}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 6}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 7}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 8}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 9}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 10}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 11}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 12}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 13}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 14}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 15}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 16}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 17}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 18}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 19}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 20}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 21}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 22}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 23}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 24}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 25}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 26}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 27}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 28}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 29}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 30}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 31}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 32}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 33}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 34}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 35}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 36}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 37}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 38}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 39}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 40}}
{"Value": "OFF", "Time": {"hour": 16, "month": 1, "second": 3.0, "year": 2017, "day": 24, "minute": 41}}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T07:59:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T07:59:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:00:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:00:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:01:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:01:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:02:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:02:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:03:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:03:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:04:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:04:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:05:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:05:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:06:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:06:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:07:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:07:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:08:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:08:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:09:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:09:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:10:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:10:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:11:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:11:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:12:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:12:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:13:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:13:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:14:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:14:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:15:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:15:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:16:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:16:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:17:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:17:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:18:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:18:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:19:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:19:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:20:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:20:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:21:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:21:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:22:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:22:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:23:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:23:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:24:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:24:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:24:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:24:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:25:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:25:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:25:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:25:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:26:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:26:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:26:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:26:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:27:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:27:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:27:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:27:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:28:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:28:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:28:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:28:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:29:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:29:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:29:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:29:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:30:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:30:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:30:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:30:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:31:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:31:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:31:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:31:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:32:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:32:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:32:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:32:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:33:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:33:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:33:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:33:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:34:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:34:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:34:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:34:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:35:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:35:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:35:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:35:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:36:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:36:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:36:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:36:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:37:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:37:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:37:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:37:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:38:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:38:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:38:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:38:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:39:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:39:00Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:39:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:39:02Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:40:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:40:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:40:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:40:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:41:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:41:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:41:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:41:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:42:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:42:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:42:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:42:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:43:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:43:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:43:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:43:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:44:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:44:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:44:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:44:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:45:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:45:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:45:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:45:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:46:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:46:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:46:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:46:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:47:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:47:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:47:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:47:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:48:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:48:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:48:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:48:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:49:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:49:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:49:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:49:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:50:00Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:50:00Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:50:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:50:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:51:01Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:51:01Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:51:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:51:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:52:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:52:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:53:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:53:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:54:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:54:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:55:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:55:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:56:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:56:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:57:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:57:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:58:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:58:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T08:59:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T08:59:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:00:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:00:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:01:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:01:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:02:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:02:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:03:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:03:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:04:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:04:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:05:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:05:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:06:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:06:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:07:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:07:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:08:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:08:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:09:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:09:02Z","value":true}
{"id":"exceeded3hPerDay","timestamp":"2017-01-30T09:10:02Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-01-30T09:10:02Z","value":true}
...
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:03:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:03:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:04:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:04:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:05:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:05:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:06:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:06:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:07:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:07:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:08:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:08:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:09:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:09:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:10:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:10:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:11:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:11:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:12:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:12:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:13:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:13:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:14:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:14:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:15:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:15:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:16:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:16:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:17:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:17:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:18:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:18:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:19:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:19:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:20:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:20:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:21:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:21:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:22:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:22:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:23:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:23:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:24:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:24:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:25:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:25:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:26:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:26:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:27:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:27:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:28:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:28:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:29:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:29:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:30:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:30:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:31:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:31:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:32:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:32:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:33:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:33:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:34:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:34:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:35:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:35:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:36:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:36:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:37:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:37:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:38:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:38:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:39:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:39:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:40:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:40:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:41:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:41:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:42:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:42:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:43:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:43:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:44:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:44:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:45:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:45:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:46:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:46:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:47:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:47:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:48:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:48:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:49:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:49:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:50:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:50:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:51:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:51:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:52:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:52:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:53:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:53:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:54:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:54:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:55:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:55:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:56:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:56:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:57:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:57:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:58:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:58:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T15:59:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T15:59:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:00:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:00:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:01:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:01:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:02:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:02:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:03:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:03:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:04:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:04:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:05:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:05:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:06:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:06:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:07:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:07:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:08:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:08:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:09:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:09:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:10:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:10:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:11:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:11:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:12:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:12:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:13:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:13:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:14:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:14:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:15:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:15:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:16:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:16:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:17:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:17:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:18:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:18:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:19:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:19:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:20:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:20:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:21:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:21:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:22:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:22:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:23:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:23:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:24:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:24:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:25:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:25:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:26:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:26:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:27:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:27:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:28:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:28:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:29:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:29:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:30:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:30:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:31:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:31:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:32:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:32:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:33:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:33:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:34:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:34:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:35:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:35:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:36:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:36:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:37:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:37:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:38:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:38:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:39:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:39:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:40:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:40:03Z","value":false}
{"id":"exceeded3hPerDay","timestamp":"2017-02-24T16:41:03Z","value":false}
{"id":"exceededAvgPlus30m","timestamp":"2017-02-24T16:41:03Z","value":false}
{"PosOutside":true,"id":"exceeded3hPerDay"}
{"PosOutside":true,"id":"exceededAvgPlus30m"}

Libraries
library STL
use library Utils 
use haskell Data.Maybe

define Streamable a => Bool mu <String funame> <Stream a x> <(a->Double) f>:
  ticks = ticksOf x
  val = (1'f cv) > 0

const filterId = Utils.filter "id" id
const filterNot = Utils.filter "not" P.not

define Bool until <(TimeDiff, TimeDiff) (a,b)> <Stream Bool x> <Stream Bool y>:
  ticks = shift (-a) y U shift (-b) y U shift (-b) x U ticksOf x
  val = let
    tnow = 1'T now
    yT = filterId y
    min_yT = if Utils.shift (-a) y [~t|False] then tnow else timeOf (Utils.shift (-a) yT >>_(b-a) t)
    xF = filterNot x
    min_xF = if not (x [~t|False]) then tnow else timeOf (xF >>_b t)
    plus x tim = 2'timeDiffPlus x 'tim
    in
    min_yT `plus` a <= tnow `plus` b && min_yT `plus` a <= min_xF

define TimeDiff alwaysaux <TimeDiff n> <Stream Bool x>:
  ticks = ticksOf x
  val = let
    nextx = 1'unT (timeOf (x>>t))
    frontier = 2'tDiffAdd nextx 'n
    in
    not cv :=> if not (x [t>|False]) then (-1) else 2'tDiff frontier now

define Bool statealways <TimeDiff n> <Stream Bool x>:
  ticks = let aaux = alwaysaux n x in delay aaux U ticksOf aaux
  val = 1'isNothing (snd cv)

define Bool always <(TimeDiff, TimeDiff) (a,b)> <Stream Bool x>:
  ticks = shift (-a) (statealways (b-a) x) U {0}
  val = let
    _this = always (a,b) x
    in 2'fromMaybe (_this [<t|True]) (fst cv)

define Bool eventually <(TimeDiff, TimeDiff) (a,b)> <Stream Bool x> =
  neg (always (a,b) (neg x))
library Utils

define (Streamable a, Streamable b) => b strMap <String funame> <(a->b) f> <Stream a s>:
  ticks = ticksOf s
  val = 1'f cv

define (Streamable a) => a filter <String funame> <(a->Bool) f> <Stream a x>:
  ticks = ticksOf x
  val = (1'f cv) :=> cv

define (Eq a, Streamable a) => a changePointsOf <Stream a s>:
  ticks = ticksOf s
  val = let
    prevMVal = s[<t|?]
    noprev = prevMVal === '-out
    prevVal = 1'getEvent prevMVal
    update = prevVal /== cv
    in noprev || update :=> cv
    where
    getEvent (Ev x) = x

define Streamable a => a firstEvOf <Stream a s>:
  ticks = ticksOf s
  val = let
    _this = firstEvOf s
    isfirst = timeOf (_this << t) === '-infty
    in isfirst :=> cv

define Streamable a => a shift <TimeDiff n> <Stream a x>:
  ticks = shift n x
  val = cv