Leaking Gaz Burner: Preconditions




Note that the greater number of control points leads to several different bounds for the leak. But the worst case is equal to the worse case found by ASPIC, the tool developped by Verimag. And the unsafe state is not entered.


C  P() {}

      PROGRAM GAZ_BURNER02

C     Check maximum leaking rate of a gaz burner: Nicolas Halbwachs and Laure Gonnord

      INTEGER T, L, X
      EXTERNAL ALEA
      LOGICAL ALEA

C  P() {}

C     BEGIN BLOCK

C  P() {}

      T = 0                                                             0001

C  P(T) {T==0}

      L = 0                                                             0002

C  P(L,T) {L==0, T==0}

      X = 0                                                             0003

C  P(L,T,X) {L==0, T==0, X==0}

      DO WHILE (.TRUE.)                                                 0004

C  P(L,T,X) {X==0, 0<=L, 6L<=T}

C        BEGIN BLOCK

C  P(L,T,X) {X==0, 0<=L, 6L<=T}

         DO WHILE (X.LE.9.AND.ALEA())                                   0005

C  P(L,T,X) {6L<=T+5X, X<=L, 0<=X, X<=9}

C           BEGIN BLOCK

C  P(L,T,X) {6L<=T+5X, X<=L, 0<=X, X<=9}

            T = T+1                                                     0006

C  P(L,T,X) {6L+1<=T+5X, X<=L, 0<=X, X<=9}

            L = L+1                                                     0007

C  P(L,T,X) {6L<=T+5X+5, X+1<=L, 0<=X, X<=9}

            X = X+1                                                     0008
C           END BLOCK
         ENDDO

C  P(L,T,X) {6L<=T+5X, X<=L, 0<=X, X<=10}

         X = 0                                                          0009

C  P(L,T,X) {X==0, 0<=L, L<=T, 6L<=T+50}

         DO WHILE (X.LE.49.OR.ALEA())                                   0010

C  P(L,T,X) {0<=L, L+X<=T, 6L+X<=T+50, 0<=X}

C           BEGIN BLOCK

C  P(L,T,X) {0<=L, L+X<=T, 6L+X<=T+50, 0<=X}

            T = T+1                                                     0011

C  P(L,T,X) {0<=L, L+X+1<=T, 6L+X<=T+49, 0<=X}

            X = X+1                                                     0012
C           END BLOCK
         ENDDO

C  P(L,T,X) {0<=L, L+X<=T, 6L+X<=T+50, 50<=X}

         X = 0                                                          0013

C  P(L,T,X) {X==0, 0<=L, L+50<=T, 6L<=T}

C        Check the leakage rate
         IF (6*L.GT.T+50) THEN                                          0014

C  P() {0==-1}

            PRINT *, "unsafe"                                           0015
         ELSE

C  P(L,T,X) {X==0, 0<=L, L+50<=T, 6L<=T}

C           BEGIN BLOCK
C           END BLOCK
         ENDIF
C        END BLOCK
      ENDDO

C     END BLOCK
      END