Difference between 'at the next time point' and 'for 1 time unit'

[leesoons]

Hi all,

I want to know if the meaning of 'at the next time point' is equivalent to 'at the next time unit', that is, equivalent to 'for 1 time unit'.

Thanks!

[tpressburger]

“for 1 tick satisfy P” means P holds now and at the next time point. “at the next timepoint satisfy P” means P holds at the next time point. Tom Pressburger NASA Ames Research Center ***@***.******@***.***> 650 604 4878 “burning for the ancient heavenly connection to the starry dynamo in the machinery of night” From: leesoons ***@***.***> Reply-To: NASA-SW-VnV/fret ***@***.***> Date: Tuesday, January 25, 2022 at 6:01 PM To: NASA-SW-VnV/fret ***@***.***> Cc: Subscribed ***@***.***> Subject: [EXTERNAL] [NASA-SW-VnV/fret] Difference between 'at the next time point' and 'for 1 time unit' (Issue #39) Hi all, I want to know if the meaning of 'at the next time point' is equivalent to 'at the next time unit', that is, equivalent to 'for 1 time unit'. Thanks! — Reply to this email directly, view it on GitHub<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FNASA-SW-VnV%2Ffret%2Fissues%2F39&data=04%7C01%7Ctom.pressburger%40nasa.gov%7C7c173c279f3b43d3124008d9e06fc73a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C637787592950344009%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ISxwRBuhtcT0nIYHGWxLjnv6s6IIhcgpzixs6tvA%2BxM%3D&reserved=0>, or unsubscribe<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAB32ZC34QU3LR45RDWM2XKTUX5IXTANCNFSM5MZ2VWFA&data=04%7C01%7Ctom.pressburger%40nasa.gov%7C7c173c279f3b43d3124008d9e06fc73a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C637787592950344009%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=zrr8L4eS0pu1AtN8PM3%2FhvDd1YKM1nAaTbmw9Rhhelg%3D&reserved=0>. Triage notifications on the go with GitHub Mobile for iOS<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7Ctom.pressburger%40nasa.gov%7C7c173c279f3b43d3124008d9e06fc73a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C637787592950344009%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=bVxpMIJ4ympjowkOCqE21bxmKxMYpAsTo%2FGBq3q4zds%3D&reserved=0> or Android<https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7Ctom.pressburger%40nasa.gov%7C7c173c279f3b43d3124008d9e06fc73a%7C7005d45845be48ae8140d43da96dd17b%7C0%7C0%7C637787592950344009%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=xTn0aVIFgrlKK8MXHAY5KvvdPfjAcq%2B4qtqgduiF8rM%3D&reserved=0>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[leesoons]

Sorry, I misunderstood the semantics of 'for'. so it means that "the next time point" actually determines the behavior of the next tick. And another question is whether the "tick" corresponds to the sampling interval of the system?

[tpressburger]

Yes. FRET generates future (and past) metric temporal logic (MTL) formalizations, where the models are sequences of discrete timepoints, so the concepts of next (and previous) timepoint applies. The language allows one to say "within 1.2 seconds" but the MTL it generates isn't really discrete time.

[leesoons]

Thanks!