[sv-ac] 1932: LTL.1932.071212.pdf. Operator precedences.

Hi,

I resend this since it didn't seem to make it to the reflector.



LTL.1932.071212.pdf partial review 2007-10-22
=============================================

Relative precedences of operators

Table 16-25
-----------

As we discussed in our meeting on 2007-11-20 I think there is reason to
change the relative precedences of the operators until, next, always,
eventually, implies, iff and |->. I tried to go through the different
combinations to see what my intuitions were and whether I could find an
ordering that would satisfy those intuitions. I see this mostly as a
point of departure for a discussion.

I came up with the following list.

next 
iff
until, implies (right associative)
|->
always, eventually, accept_on, reject_on

Following is a list of pairs of operators and their relative order
according to the list above. After the colon is a reference to a
discussion/motivation of that particular pair further below.

next over iff: 1 
next over until: 1 
next over implies: 1 
next over |->: 3 (1,7)
next over always,eventually,accept_on,reject_on: 4 (1,12)
iff over until: 10
iff over implies: 5 (10,6)
iff over |->: 7
iff over always,eventually: 8
iff over accept_on,reject_on: 9
until same level as implies: 6
until over |->: 7
until over always,eventually: 12
until over accept_on,reject_on: 13
implies over |->: 7
implies over always,eventually: 8
implies over accept_on,reject_on: 9
|-> over always/eventually/accept_on/reject_on: 14


1) next vs. implies/iff/until
----------------------------
1.a.1) next F implies/iff/until P => (next F) implies/iff/until P
1.a.2)                            => next (F implies/iff/until P)
1.b) F implies/iff/until next P   => F implies/iff/until (next P)

I think users will more often mean (1.a.1) than (1.a.2), but this is not
a strong intuition of mine. With regard to (b) there seems to be only
one possible resolution.


3) next vs. |->
-----------------
3.a.1) next r |-> P       => (next r) |-> P
3.a.2)                   => next (r |-> P)
3.b) r |-> next P         => r |-> (next P)

3.a.1 is not possible because it is a syntax error. So the relative
precedence of next and |-> does not matter. On the other hand I think
there are reasons to put until over |-> (7) and next over
until (1).


4) next vs. always, eventually, accept_on, reject_on
-----------------------------------------------------
The relative precedences here don't seem to matter since all these
operators are prefix. But see 1 and 12.


5) implies vs. iff
-------------------
5.a.1) F implies P iff Q       => (F implies P) iff Q 
5.a.2)                         => F implies (P iff Q)
5.b.1) F iff P implies Q       => F iff (P implies Q)
5.b.2)                         => (F iff P) implies Q

I have no strong intuition either way here. However there are reasons to
put iff over until (10) and also to put until and implies on the same
level (6),


6) implies vs. until
---------------------
6.a.1) F implies P until Q       => (F implies P) until Q 
6.a.2)                           => F implies (P until Q)
6.b.1) F until P implies Q       => F until (P implies Q)
6.b.2)                           => (F until P) implies Q

Intuitively I prefer 6.a.2 over 6.a.1 but on the other hand I prefer
6.b.1 over 6.b.2. We may put them on the same precedence level and make
them right associative.


7) implies/iff/until vs. |->
---------------------
7.a.1) F implies/iff/until r |-> Q       => (F implies/iff/until r) |-> Q 
7.a.2)                           => F implies/iff/until (r |-> Q)
7.b.1) r |-> P implies/iff/until Q       => r |-> (P implies/iff/until Q)
7.b.2)                           => (r |-> P) implies/iff/until Q

7.a.1 is impossible (syntax error) and I prefer 7.b.1
over 7.b.2.

8) implies/iff vs. always/eventually
---------------------------------
8.a) F implies/iff always/eventually P   => F implies/iff (always/eventually P) 
8.b.1) always/eventually F implies/iff Q => always/eventually (F implies/iff Q)
8.b.2)                               => (always/eventually F) implies/iff Q 

I rather strongly prefer 8.b.1 over 8.b.2 here.

9) implies/iff vs. accept_on/reject_on
-----------------------------------
9.a) F implies/iff accept_on/reject_on P   => F implies/iff (accept_on/reject_on P) 
9.b.1) accept_on/reject_on F implies/iff Q => accept_on/reject_on (F implies/iff Q)
9.b.2)                               => (accept_on/reject_on F) implies/iff Q 

I prefer 9.b.1 over 9.b.2 here.


10) iff vs. until
---------------------
10.a.1) F iff P until Q       => (F iff P) until Q 
10.a.2)                           => F iff (P until Q)
10.b.1) F until P iff Q       => F until (P iff Q)
10.b.2)                           => (F until P) iff Q

I prefer 10.a.1 to 10.a.2 and 10.b.1 to 1o.b.2



12) until vs. always/eventually
---------------------------------
12.a) F until always/eventually P   => F until (always/eventually P) 
12.b.1) always/eventually F until Q => always/eventually (F until Q)
12.b.2)                             => (always/eventually F) until Q 

I rather strongly prefer 12.b.1 over 12.b.2 here.

13) until vs. accept_on/reject_on
-----------------------------------
13.a) F until accept_on/reject_on P   => F until (accept_on/reject_on P) 
13.b.1) accept_on/reject_on F until Q => accept_on/reject_on (F until Q)
13.b.2)                               => (accept_on/reject_on F) until Q 

I rather strongly prefer 13.b.1 over 13.b.2 here.

14) |-> vs. always/eventually/accept_on/reject_on
---------------------------------
14.a) r |-> always/eventually P   => r |-> (always/eventually P) 
14.b.1) always/eventually r |-> Q => always/eventually (r |-> Q)
14.b.2)                             => (always/eventually r) |-> Q 

14.b.1 is impossible because it is a syntax error, hence the relative
precedence of |-> and always/eventually/accept_on/reject_on is not
important

15) |-> vs. accept_on/reject_on
-----------------------------------
15.a) r |-> accept_on/reject_on P     => r |-> (accept_on/reject_on P) 
15.b.1) accept_on/reject_on r |-> Q   => accept_on/reject_on (r |-> Q)
15.b.2)                               => (accept_on/reject_on r) |-> Q 

I rather strongly prefer 15.b.1 over 15.b.2 here (15.b.2 is a syntax
error).


------------------------



Best Regards,

Johan M







-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Kvarnbergsgatan 2                Fax: +46 31 7451914
411 05 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.