copilot-libraries: implementation of PTLTL operator since is non-standard

[InnovativeInventor]

There appears to be a subtle bug in the definition of since in PTLTL.hs.

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

Lines 42 to 46 in 9e2b8ff

	-- | 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

since is an existential claim; it should be true when there exists any prior period in which s2 holds and after which s1 continuously holds.^{1 2 3} However, the since operator defined in PTLTL.hs will only listen for the first true value in s2, which is incorrect.

The following is a self-contained definition of since that is more correct.

ever :: Stream Bool -> Stream Bool
ever s = go
  where
    go = s || ([False] ++ go)


globally :: Stream Bool -> Stream Bool
globally s = go
  where 
    go = s && ([True] ++ go)
    
implies :: Stream Bool -> Stream Bool -> Stream Bool
implies s1 s2 = not (s1 && (not s2))

-- n is the current pos, s1 and s2 are array-like
-- spec: exists i <= n. (s2_i and forall j >= n. s1_j)
sinceMine :: Stream Bool -> Stream Bool -> Stream Bool
sinceMine s1 s2 = ever (implies s2 (globally s1))

Note that the corrected since definition will look for any point s2 is true and after which s1 holds.

Counterexample stream

The following is a counterexample input stream and specification on which sinceMine (defined above) is more correct than the since operator (defined in PTLTL.hs.

Counterexample input and specification

module Main where

import Language.Copilot hiding  (alwaysBeen, eventuallyPrev, since)

import Prelude ()

-- from Copilot lang, PTLTL.hs
-- | Did @s@ hold in the previous period?
previous :: Stream Bool -> Stream Bool
previous s = [ False ] ++ s

-- | Has @s@ always held (up to and including the current state)?
alwaysBeen :: Stream Bool -> Stream Bool
alwaysBeen s = s && tmp
    where
      tmp = [ True ] ++ s && tmp

-- | Did @s@ hold at some time in the past (including the current state)?
eventuallyPrev :: Stream Bool -> Stream Bool
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

-- everything below is my derivation
ever :: Stream Bool -> Stream Bool
ever s = go -- limitation with GHC?
  where
    go = s || ([False] ++ go)


globally :: Stream Bool -> Stream Bool
globally s = go
  where 
    go = s && ([True] ++ go)
    
implies :: Stream Bool -> Stream Bool -> Stream Bool
implies s1 s2 = not (s1 && (not s2))

-- n is the current pos, s1 and s2 are array-like
-- spec: exists i <= n. (s1_i and forall j >= n. s2_j)
sinceMine :: Stream Bool -> Stream Bool -> Stream Bool
sinceMine s1 s2 = ever (implies s2 (globally s1))

specCounterexample = do
  observer "input1" input1
  observer "input2" input2
  observer "since input1 input2" (since input1 input2)
  observer "sinceMine input1 input2" (sinceMine 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 specCounterexample

Output of input and counterexample specification

input1:                   input2:                   since input1 input2:      sinceMine input1 input2: 
true                      false                     true                      true                     
true                      true                      true                      true                     
false                     true                      false                     true                     
true                      true                      false                     true                     
true                      false                     false                     true                     
true                      false                     false                     true                     
true                      false                     false                     true                     
true                      false                     false                     true                     
true                      false                     false                     true                     
true                      false                     false                     true                     

since, as defined in the literature, should return true for the entire stream. At any given point, there is a prior period in which input2 is true and after which input1 is continuously true. However, the since implementation in PTLTL.hs does not return true for the entire stream.

Footnotes

1. See page 198. Orna Lichtenstein, Amir Pnueli, and Lenor Zuck. 1985. The glory of the past. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_16 ↩

2. See page 59. Rajeev Alur and Thomas A. Henzinger. 1993. Real-Time Logics: Complexity and Expressiveness. Information and Computation, Volume 104, Issue 1. https://doi.org/10.1006/inco.1993.1025. ↩

3. See page 9. Johan Anthony Wilem Kamp. (1968). Tense Logic and the Theory of Linear Order. Ph.D. Dissertation. University of California Los Angles, Los Angles, CA. https://www.proquest.com/openview/408039eb4ed228dc4cba3fe7e1774163/1?pq-origsite=gscholar&cbl=18750&diss=y#. ↩

[ivanperez-keera]

Description

The function Copilot.Library.PTLTL.since, which should implement the since temporal operator, does not behave as is standard in the literature.

In the standard definition, since phi1 phi2 should be true if phi1 has continuously been true since the last time that phi2 has been true. However, in Copilot, since phi1 phi2 is true if phi1 has continuously been true since the first time that phi2 has been true.

Type

• Bug: operator in Copilot does not conform to intended meaning.

Additional context

• See page 198. Orna Lichtenstein, Amir Pnueli, and Lenor Zuck. 1985. The glory of the past. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_16
• See page 59. Rajeev Alur and Thomas A. Henzinger. 1993. Real-Time Logics: Complexity and Expressiveness. Information and Computation, Volume 104, Issue 1. https://doi.org/10.1006/inco.1993.1025.
• See page 9. Johan Anthony Wilem Kamp. (1968). Tense Logic and the Theory of Linear Order. Ph.D. Dissertation. University of California Los Angles, Los Angles, CA. https://www.proquest.com/openview/408039eb4ed228dc4cba3fe7e1774163/1?pq-origsite=gscholar&cbl=18750&diss=y#.

Requester

• Max Fan (NASA)

Method to check presence of bug

The following Copilot spec:

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

Behaves differently with the current vs the expected implementation of since. with the current one, only the the first two outputs are true, but it should always be true.

Expected result

The implementation of since conforms to the standard definition in the literature.

The spec above should print:

output: 
true    
true    
true    
true    
true    
true    
true    
true    
true    
true    

Desired result

The implementation of since conforms to the standard definition in the literature.

The spec above should print:

output: 
true    
true    
true    
true    
true    
true    
true    
true    
true    
true    

Proposed solution

Modify the implementation of Copilot.Library.PTLTL.since so that since phi1 phi2 is true if phi1 has continuously been true since the last time that phi2 has been true.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 3.16.1.

Fix assigned to: @InnovativeInventor .

EDIT: Milestone was renamed 3.16.1 upon release. It was originally named 3.17.

[InnovativeInventor]

Implementor: Solution implemented, review requested.

[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).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.