You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Oct 28, 2019. It is now read-only.
After #81, we've got a good coverage of the Dwyer adaptations of linear temporal logic, but we could do better. Some ideas:
Alternatives of since/after/before/until that take timepoints. Right now users would have to do .travelInTime(timepoint).since(...), so it's not too important but it would be nice for conciseness.
weakBefore / weakUntil, which go up to the end of the history instead of returning null if a matching version does not exist.
xAnnotated could take an optional second argument with the value of interest: it does not necessarily have to be true.
Negated when: unless.
Chains of events: whenChain((v1 | P1), ...., (vN | PN)) looks for cases when P1 is followed by P2, then by P3, and so on until PN. This could be done for the temporal assertions (e.g. always will check that for each of those versions, you always get that chain of events).
The current implementations return null when no matches happen, which would make something like x.when(v|condition which is always false).always(v|something else) not work, when conceptually it should return true (empty proof). It might be better to return a smarter marker value that the various primitives understand (e.g. an empty collection). always(...) and never(...) would trivially return true in this situation, and eventually* would return false for these markers. Continuing to call when(...) or any other filtering operations would just propagate the empty collection.
Rather than have all these various when / whenAnnotated / whenChain options, it would be good to simply take when and have it overloaded for all the various types of arguments. Same for the rest of the primitives.
I'll write down more ideas as I come up with them.
The text was updated successfully, but these errors were encountered:
After #81, we've got a good coverage of the Dwyer adaptations of linear temporal logic, but we could do better. Some ideas:
.travelInTime(timepoint).since(...)
, so it's not too important but it would be nice for conciseness.weakBefore
/weakUntil
, which go up to the end of the history instead of returningnull
if a matching version does not exist.xAnnotated
could take an optional second argument with the value of interest: it does not necessarily have to betrue
.when
:unless
.whenChain((v1 | P1), ...., (vN | PN))
looks for cases when P1 is followed by P2, then by P3, and so on until PN. This could be done for the temporal assertions (e.g.always
will check that for each of those versions, you always get that chain of events).null
when no matches happen, which would make something likex.when(v|condition which is always false).always(v|something else)
not work, when conceptually it should returntrue
(empty proof). It might be better to return a smarter marker value that the various primitives understand (e.g. an empty collection).always(...)
andnever(...)
would trivially returntrue
in this situation, andeventually*
would returnfalse
for these markers. Continuing to callwhen(...)
or any other filtering operations would just propagate the empty collection.when
/whenAnnotated
/whenChain
options, it would be good to simply takewhen
and have it overloaded for all the various types of arguments. Same for the rest of the primitives.I'll write down more ideas as I come up with them.
The text was updated successfully, but these errors were encountered: