0 votes

Hi,

In the figure given below, Can you explain why does NOT c & [(Fb) SU (¬a ∧ Xa)] hold in s0 ? We are getting (!a & X a) in s1 so the strong until would hold in s1.

in * TF "Emb. Sys. and Rob." by (1.4k points)

1 Answer

+1 vote
 
Best answer

Look at the following trace:

                        s0 s1 s2 ...
                    a : 0  0  1  ...
                    b : 0  0  0  ...
                    c : 1  0  0  ...
             !a & X a : 0  1  0  ...
                  F b : 0  0  0  ...
    [F b SU !a & X a] : 0  1  0  ...
      [b SU !a & X a] : 0  1  0  ...
     F[b SU !a & X a] : 1  1  0  ...

    

by (91.8k points)
selected by
Interesting, does this imply F b SU a is equivelant to  b SU a?
No, that is not true, we do not even have [(F b) SU a] -> [b SU a] as can be seen as follows:

                  a : 0 0 1 0 0 1...
                  b : 1 0 0 1 0 0 ...
       [b SU a] : 0 0 1 0 0 1...
               F b : 1 1 1 1 ...
  [(F b) SU a] : 1 1 1
Oh ok thanks alot

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked Jan 26 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
0 votes
1 answer
asked Feb 5 in * TF "Emb. Sys. and Rob." by dn (1.4k points)
Imprint | Privacy Policy
...