A correction to the answer to Exercise 2.3 (January 19--20, 2005) ----------------------------------------------------------------- The number of cases in the case graph of the first C/E-system is 30, thus not 13. The number of cases in the case graph of the second C/E-system is still 8 as claimed. In order to conclude that the systems are not equivalent, it suffices to find out that the case graph of the first system has more cases than the case graph of the second system. So, it is not necessary to construct the whole case graph for the first system. In the session below, PROD constructs reachability graphs for nets that simulate the above-mentioned C/E-systems "in an appropriate way". The places hq, hr, hs, hu and hv are complement places for the places q, r, s, u and v. The transitions ia, ib, ic, id and ie are inverse transitions for the transitions a, b, c, d and e. The effect of non-singleton steps is not simulated because singleton steps determine the number of cases in a case graph. The way of simulation ensures the following, the proof of which is omitted for convenience: (1) The number of nodes in the reachability graph of r_2_3_1.net is equal to the number of cases in the case graph of the first C/E-system. (2) The number of nodes in the reachability graph of r_2_3_2.net is equal to the number of cases in the case graph of the second C/E-system. Script started on Sun Mar 6 12:28:53 2005 kva@debian 101: cat r2_3.sh #!/bin/bash -x diff r2_3_1.net r2_3_2.net set -e for k in 1 2 ; do f=r2_3_$k cat $f.net prod $f.init ./$f echo 'statistics' > $f.btc echo 'showends all succs' >> $f.btc echo 'quit' >> $f.btc probe -e $f < $f.btc rm -f $f.btc prod $f.clean done kva@debian 102: ./r2_3.sh + diff r2_3_1.net r2_3_2.net 28,29c28,29 < in { u: <..>; hv: <..>; } < out { hu: <..>; v: <..>; } --- > in { hs: <..>; u: <..>; } > out { s: <..>; hu: <..>; } 48,49c48,49 < in { hu: <..>; v: <..>; } < out { u: <..>; hv: <..>; } --- > in { s: <..>; hu: <..>; } > out { hs: <..>; u: <..>; } + set -e + for k in 1 2 + f=r2_3_1 + cat r2_3_1.net #place q #place r #place s mk(<..>) #place u #place v mk(<..>) #place hq mk(<..>) #place hr mk(<..>) #place hs #place hu mk(<..>) #place hv #trans a in { hq: <..>; s: <..>; v: <..>; } out { q: <..>; hs: <..>; hv: <..>; } #endtr #trans b in { q: <..>; hr: <..>; } out { hq: <..>; r: <..>; } #endtr #trans c in { r: <..>; hs: <..>; } out { hr: <..>; s: <..>; } #endtr #trans d in { q: <..>; hu: <..>; } out { hq: <..>; u: <..>; } #endtr #trans e in { u: <..>; hv: <..>; } out { hu: <..>; v: <..>; } #endtr #trans ia in { q: <..>; hs: <..>; hv: <..>; } out { hq: <..>; s: <..>; v: <..>; } #endtr #trans ib in { hq: <..>; r: <..>; } out { q: <..>; hr: <..>; } #endtr #trans ic in { hr: <..>; s: <..>; } out { r: <..>; hs: <..>; } #endtr #trans id in { hq: <..>; u: <..>; } out { q: <..>; hu: <..>; } #endtr #trans ie in { hu: <..>; v: <..>; } out { u: <..>; hv: <..>; } #endtr + prod r2_3_1.init + ./r2_3_1 + echo statistics + echo 'showends all succs' + echo quit + probe -e r2_3_1 0#statistics Number of nodes: 30 Number of arrows: 72 Number of terminal nodes: 0 Number of nodes that have been completely processed: 30 Strongly connected components have not been computed 0#showends all succs Node 0 s: <..> v: <..> hq: <..> hr: <..> hu: <..> ------------------------------------------------ Arrow 0: transition a, precedence class 0 to node 1 ------------------------------------------------ Arrow 1: transition ic, precedence class 0 to node 2 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 3 ------------------------------------------------ Node 0 has 3 successor arrows ------------------------------------------------ Node 1 q: <..> hr: <..> hs: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 4 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 5 ------------------------------------------------ Arrow 2: transition ia, precedence class 0 to node 0 ------------------------------------------------ Node 1 has 3 successor arrows ------------------------------------------------ Node 2 r: <..> v: <..> hq: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 0 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 6 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 7 ------------------------------------------------ Node 2 has 3 successor arrows ------------------------------------------------ Node 3 s: <..> u: <..> hq: <..> hr: <..> hv: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 0 ------------------------------------------------ Arrow 1: transition ic, precedence class 0 to node 7 ------------------------------------------------ Arrow 2: transition id, precedence class 0 to node 8 ------------------------------------------------ Node 3 has 3 successor arrows ------------------------------------------------ Node 4 r: <..> hq: <..> hs: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 9 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 1 ------------------------------------------------ Node 4 has 2 successor arrows ------------------------------------------------ Node 5 u: <..> hq: <..> hr: <..> hs: <..> hv: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 10 ------------------------------------------------ Arrow 1: transition id, precedence class 0 to node 1 ------------------------------------------------ Node 5 has 2 successor arrows ------------------------------------------------ Node 6 q: <..> v: <..> hr: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 2 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 11 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 12 ------------------------------------------------ Node 6 has 3 successor arrows ------------------------------------------------ Node 7 r: <..> u: <..> hq: <..> hs: <..> hv: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 3 ------------------------------------------------ Arrow 1: transition e, precedence class 0 to node 2 ------------------------------------------------ Arrow 2: transition ib, precedence class 0 to node 12 ------------------------------------------------ Arrow 3: transition id, precedence class 0 to node 13 ------------------------------------------------ Node 7 has 4 successor arrows ------------------------------------------------ Node 8 q: <..> s: <..> hr: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 14 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 3 ------------------------------------------------ Arrow 2: transition ic, precedence class 0 to node 13 ------------------------------------------------ Node 8 has 3 successor arrows ------------------------------------------------ Node 9 s: <..> hq: <..> hr: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition ic, precedence class 0 to node 4 ------------------------------------------------ Node 9 has 1 successor arrows ------------------------------------------------ Node 10 v: <..> hq: <..> hr: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition ie, precedence class 0 to node 5 ------------------------------------------------ Node 10 has 1 successor arrows ------------------------------------------------ Node 11 u: <..> v: <..> hq: <..> hr: <..> hs: <..> ------------------------------------------------ Arrow 0: transition id, precedence class 0 to node 6 ------------------------------------------------ Node 11 has 1 successor arrows ------------------------------------------------ Node 12 q: <..> u: <..> hr: <..> hs: <..> hv: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 7 ------------------------------------------------ Arrow 1: transition e, precedence class 0 to node 6 ------------------------------------------------ Arrow 2: transition ia, precedence class 0 to node 15 ------------------------------------------------ Node 12 has 3 successor arrows ------------------------------------------------ Node 13 q: <..> r: <..> hs: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 8 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 7 ------------------------------------------------ Arrow 2: transition ia, precedence class 0 to node 16 ------------------------------------------------ Node 13 has 3 successor arrows ------------------------------------------------ Node 14 r: <..> s: <..> hq: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition ib, precedence class 0 to node 8 ------------------------------------------------ Node 14 has 1 successor arrows ------------------------------------------------ Node 15 s: <..> u: <..> v: <..> hq: <..> hr: <..> ------------------------------------------------ Arrow 0: transition a, precedence class 0 to node 12 ------------------------------------------------ Arrow 1: transition ic, precedence class 0 to node 17 ------------------------------------------------ Arrow 2: transition id, precedence class 0 to node 18 ------------------------------------------------ Node 15 has 3 successor arrows ------------------------------------------------ Node 16 r: <..> s: <..> v: <..> hq: <..> hu: <..> ------------------------------------------------ Arrow 0: transition a, precedence class 0 to node 13 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 18 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 19 ------------------------------------------------ Node 16 has 3 successor arrows ------------------------------------------------ Node 17 r: <..> u: <..> v: <..> hq: <..> hs: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 15 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 20 ------------------------------------------------ Arrow 2: transition id, precedence class 0 to node 21 ------------------------------------------------ Node 17 has 3 successor arrows ------------------------------------------------ Node 18 q: <..> s: <..> v: <..> hr: <..> hu: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 16 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 15 ------------------------------------------------ Arrow 2: transition ic, precedence class 0 to node 21 ------------------------------------------------ Arrow 3: transition ie, precedence class 0 to node 22 ------------------------------------------------ Node 18 has 4 successor arrows ------------------------------------------------ Node 19 r: <..> s: <..> u: <..> hq: <..> hv: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 16 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 22 ------------------------------------------------ Arrow 2: transition id, precedence class 0 to node 23 ------------------------------------------------ Node 19 has 3 successor arrows ------------------------------------------------ Node 20 q: <..> u: <..> v: <..> hr: <..> hs: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 17 ------------------------------------------------ Node 20 has 1 successor arrows ------------------------------------------------ Node 21 q: <..> r: <..> v: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 18 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 17 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 24 ------------------------------------------------ Node 21 has 3 successor arrows ------------------------------------------------ Node 22 q: <..> s: <..> u: <..> hr: <..> hv: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 19 ------------------------------------------------ Arrow 1: transition e, precedence class 0 to node 18 ------------------------------------------------ Arrow 2: transition ic, precedence class 0 to node 24 ------------------------------------------------ Node 22 has 3 successor arrows ------------------------------------------------ Node 23 q: <..> r: <..> s: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition d, precedence class 0 to node 19 ------------------------------------------------ Node 23 has 1 successor arrows ------------------------------------------------ Node 24 q: <..> r: <..> u: <..> hs: <..> hv: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 22 ------------------------------------------------ Arrow 1: transition e, precedence class 0 to node 21 ------------------------------------------------ Arrow 2: transition ia, precedence class 0 to node 25 ------------------------------------------------ Node 24 has 3 successor arrows ------------------------------------------------ Node 25 r: <..> s: <..> u: <..> v: <..> hq: <..> ------------------------------------------------ Arrow 0: transition a, precedence class 0 to node 24 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 26 ------------------------------------------------ Arrow 2: transition id, precedence class 0 to node 27 ------------------------------------------------ Node 25 has 3 successor arrows ------------------------------------------------ Node 26 q: <..> s: <..> u: <..> v: <..> hr: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 25 ------------------------------------------------ Arrow 1: transition ic, precedence class 0 to node 28 ------------------------------------------------ Node 26 has 2 successor arrows ------------------------------------------------ Node 27 q: <..> r: <..> s: <..> v: <..> hu: <..> ------------------------------------------------ Arrow 0: transition d, precedence class 0 to node 25 ------------------------------------------------ Arrow 1: transition ie, precedence class 0 to node 29 ------------------------------------------------ Node 27 has 2 successor arrows ------------------------------------------------ Node 28 q: <..> r: <..> u: <..> v: <..> hs: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 26 ------------------------------------------------ Node 28 has 1 successor arrows ------------------------------------------------ Node 29 q: <..> r: <..> s: <..> u: <..> hv: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 27 ------------------------------------------------ Node 29 has 1 successor arrows ------------------------------------------------ 30 nodes (all) ------------------------------------------------ 0#quit + rm -f r2_3_1.btc + prod r2_3_1.clean + for k in 1 2 + f=r2_3_2 + cat r2_3_2.net #place q #place r #place s mk(<..>) #place u #place v mk(<..>) #place hq mk(<..>) #place hr mk(<..>) #place hs #place hu mk(<..>) #place hv #trans a in { hq: <..>; s: <..>; v: <..>; } out { q: <..>; hs: <..>; hv: <..>; } #endtr #trans b in { q: <..>; hr: <..>; } out { hq: <..>; r: <..>; } #endtr #trans c in { r: <..>; hs: <..>; } out { hr: <..>; s: <..>; } #endtr #trans d in { q: <..>; hu: <..>; } out { hq: <..>; u: <..>; } #endtr #trans e in { hs: <..>; u: <..>; } out { s: <..>; hu: <..>; } #endtr #trans ia in { q: <..>; hs: <..>; hv: <..>; } out { hq: <..>; s: <..>; v: <..>; } #endtr #trans ib in { hq: <..>; r: <..>; } out { q: <..>; hr: <..>; } #endtr #trans ic in { hr: <..>; s: <..>; } out { r: <..>; hs: <..>; } #endtr #trans id in { hq: <..>; u: <..>; } out { q: <..>; hu: <..>; } #endtr #trans ie in { s: <..>; hu: <..>; } out { hs: <..>; u: <..>; } #endtr + prod r2_3_2.init + ./r2_3_2 + echo statistics + echo 'showends all succs' + echo quit + probe -e r2_3_2 0#statistics Number of nodes: 8 Number of arrows: 18 Number of terminal nodes: 0 Number of nodes that have been completely processed: 8 Strongly connected components have not been computed 0#showends all succs Node 0 s: <..> v: <..> hq: <..> hr: <..> hu: <..> ------------------------------------------------ Arrow 0: transition a, precedence class 0 to node 1 ------------------------------------------------ Arrow 1: transition ic, precedence class 0 to node 2 ------------------------------------------------ Arrow 2: transition ie, precedence class 0 to node 3 ------------------------------------------------ Node 0 has 3 successor arrows ------------------------------------------------ Node 1 q: <..> hr: <..> hs: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 4 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 5 ------------------------------------------------ Arrow 2: transition ia, precedence class 0 to node 0 ------------------------------------------------ Node 1 has 3 successor arrows ------------------------------------------------ Node 2 r: <..> v: <..> hq: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 0 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 6 ------------------------------------------------ Node 2 has 2 successor arrows ------------------------------------------------ Node 3 u: <..> v: <..> hq: <..> hr: <..> hs: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 0 ------------------------------------------------ Arrow 1: transition id, precedence class 0 to node 6 ------------------------------------------------ Node 3 has 2 successor arrows ------------------------------------------------ Node 4 r: <..> hq: <..> hs: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition c, precedence class 0 to node 7 ------------------------------------------------ Arrow 1: transition ib, precedence class 0 to node 1 ------------------------------------------------ Node 4 has 2 successor arrows ------------------------------------------------ Node 5 u: <..> hq: <..> hr: <..> hs: <..> hv: <..> ------------------------------------------------ Arrow 0: transition e, precedence class 0 to node 7 ------------------------------------------------ Arrow 1: transition id, precedence class 0 to node 1 ------------------------------------------------ Node 5 has 2 successor arrows ------------------------------------------------ Node 6 q: <..> v: <..> hr: <..> hs: <..> hu: <..> ------------------------------------------------ Arrow 0: transition b, precedence class 0 to node 2 ------------------------------------------------ Arrow 1: transition d, precedence class 0 to node 3 ------------------------------------------------ Node 6 has 2 successor arrows ------------------------------------------------ Node 7 s: <..> hq: <..> hr: <..> hu: <..> hv: <..> ------------------------------------------------ Arrow 0: transition ic, precedence class 0 to node 4 ------------------------------------------------ Arrow 1: transition ie, precedence class 0 to node 5 ------------------------------------------------ Node 7 has 2 successor arrows ------------------------------------------------ 8 nodes (all) ------------------------------------------------ 0#quit + rm -f r2_3_2.btc + prod r2_3_2.clean kva@debian 103: exit Script done on Sun Mar 6 12:30:26 2005