copilot-libraries: Fix semantics of since in Copilot.Library.PTLTL. Refs #443.

[InnovativeInventor]

Fix the semantics of since to be true if there exists any point at which s2 holds and after which s1 continuously holds, as prescribed in the solution proposed for #443.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:

  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/264840733

  • The solution proposed produces the expected result. Details:

    The following Dockerfile checks that the implementation of since produces true if the first argument is true since the last time the second argument was true (not since the first), as expected based on its formal definition. In that case, it prints the message Success:

    --- Dockerfile
    FROM ubuntu:trusty
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN apt-get install --yes git
    
    ADD Spec.hs /tmp/Spec.hs
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-install alex happy \
      && cabal v1-install $NAME/copilot**/ \
      && (cabal v1-exec -- runhaskell /tmp/Spec.hs > /dev/null 2>&1) \
      && ! (cabal v1-exec -- runhaskell /tmp/Spec.hs | grep false) \
      && echo "Success"
    
    --- Spec.hs
    module Main where
    
    import Language.Copilot
    import Prelude hiding ((++))
    
    spec :: Spec
    spec = do
        observer "output" (since input1 input2)
      where
        input1 = [True, True, False, True, True] ++ true
        input2 = [False, True, True, True, False] ++ false
    
    -- Interpret the spec for 10 ticks
    main = interpret 10 spec

    Command (substitute variables based on new path after merge):

    $ docker run -e "REPO=https://github.com/innovativeinvetor/copilot" -e "NAME=copilot" -e "COMMIT=54853d7db4ff42b106c10e953c44f7aa58273806" -it copilot-verify-443

• Implementation is documented. Details:
  Haddock documentation is adjusted.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed.
• Required version bumps are evaluated. Details:
  Bump not needed: although the meaning of the function does change, the change makes the function conform to its expected meaning, so it's considered a non-breaking change (rather, it's a bug fix).