copilot-libraries: Fix semantics of since in PTLTL.hs. Close Copilot-…

…Language#443.

The current implementation of `Copilot.Library.PTLTL.since` does not
conform to the standard semantics of since, as a temporal operator.
`since` is an existential claim; it must be true when there exists *any*
prior period in which s2 holds and before which s1 has been continuously
true. The current implementation only looks for the first time s2 is
true, which is non-standard.

This commit fixes the implementation and updates the comment to reflect
the correct semantics.

copilot-libraries/src/Copilot/Library/PTLTL.hs

@@ -39,8 +39,6 @@ eventuallyPrev s = s || tmp
   where
     tmp = [ False ] ++ s || tmp
 
--- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?
-since ::  Stream Bool -> Stream Bool -> Stream Bool
-since s1 s2 = alwaysBeen ( tmp ==> s1 )
-    where
-      tmp = eventuallyPrev $ [ False ] ++ s2
+-- | Is there a time when @s2@ holds and before which @s1@ continuously holds?
+since :: Stream Bool -> Stream Bool -> Stream Bool
+since s1 s2 = eventuallyPrev (s2 ==> (alwaysBeen s1))