Yes we need to figure out how to interleave the rest of the operators in this ordering of the new ones. My hunch is that not should be at the same level as next, and and or between next and iff and if-else at the bottom together with always, eventually, accept_on and reject_on. We would then end up with something like next, not and or iff until, implies (right associative) |-> always, eventually, accept_on, reject_on, if-else Best Reagards, Johan On Sun, Dec 23, 2007 at 08:56:15AM +0200, Bustan, Doron wrote: > Johan, > > Thanks for an exhaustive work. > I don't disagree with any of you intuitions and agree with some. > Where would you put if-else? > > Doron > > > >>-----Original Message----- > >>From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On > >>Behalf Of Johan M?rtensson > >>Sent: Thursday, December 20, 2007 11:10 AM > >>To: sv-ac@server.eda.org > >>Cc: Bustan, Doron > >>Subject: [sv-ac] 1932: LTL.1932.071212.pdf. Operator precedences. > >> > >>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. > > --------------------------------------------------------------------- > Intel Israel (74) Limited > > This e-mail and any attachments may contain confidential material for > the sole use of the intended recipient(s). Any review or distribution > by others is strictly prohibited. If you are not the intended > recipient, please contact the sender and delete all copies. > -- ------------------------------------------------------------ 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.Received on Sun Dec 23 04:39:54 2007
This archive was generated by hypermail 2.1.8 : Sun Dec 23 2007 - 04:40:38 PST