# HG changeset patch
# User mueller
# Date 869136298 -7200
# Node ID 23eae933c2d90f7f25ac0f84d5b8bd7149478c8a
# Parent  a34c20f4bf442e7847d2e3a11d6d9dc89216d72b
changes needed for introducing fairness

diff -r a34c20f4bf44 -r 23eae933c2d9 src/HOLCF/IOA/NTP/Abschannel.ML
--- a/src/HOLCF/IOA/NTP/Abschannel.ML	Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML	Thu Jul 17 12:44:58 1997 +0200
@@ -10,7 +10,7 @@
 
 val unfold_renaming = 
  [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
-   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, 
+   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, 
    actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, 
    trans_of_def] @ asig_projections;
 
@@ -43,11 +43,17 @@
 by(simp_tac (!simpset addsimps unfold_renaming) 1);
 qed"in_rsch_asig";
 
-goal Abschannel.thy "srch_ioa = (srch_asig, {{|}}, srch_trans)";
+goal Abschannel.thy "srch_ioa = \
+\   (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)";
+by (simp_tac (!simpset addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
+              wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
 by(simp_tac (!simpset addsimps unfold_renaming) 1);
 qed"srch_ioa_thm";
 
-goal Abschannel.thy "rsch_ioa = (rsch_asig, {{|}}, rsch_trans)";
+goal Abschannel.thy "rsch_ioa = \
+\    (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)";
+by (simp_tac (!simpset addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
+              wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
 by(simp_tac (!simpset addsimps unfold_renaming) 1);
 qed"rsch_ioa_thm";
 
diff -r a34c20f4bf44 -r 23eae933c2d9 src/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOLCF/IOA/NTP/Abschannel.thy	Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Abschannel.thy	Thu Jul 17 12:44:58 1997 +0200
@@ -24,6 +24,9 @@
 srch_asig, 
 rsch_asig  :: 'm action signature
 
+srch_wfair, srch_sfair, rsch_sfair,
+rsch_wfair ::('m action)set set
+
 srch_trans :: ('m action, 'm packet multiset)transition set
 rsch_trans :: ('m action, bool multiset)transition set
 
@@ -39,6 +42,12 @@
 srch_trans_def "srch_trans == trans_of(srch_ioa)"  
 rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
 
+srch_wfair_def "srch_wfair == wfair_of(srch_ioa)"  
+rsch_wfair_def "rsch_wfair == wfair_of(rsch_ioa)"
+
+srch_sfair_def "srch_sfair == sfair_of(srch_ioa)"  
+rsch_sfair_def "rsch_sfair == sfair_of(rsch_ioa)"
+
 srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
 rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
 
@@ -53,7 +62,7 @@
         of S(b) => t = addm s b |                            
            R(b) => count s b ~= 0 & t = delm s b}"
 
-ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
+ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans,{},{})"
 
 
 rsch_actions_def "rsch_actions (akt) ==        
diff -r a34c20f4bf44 -r 23eae933c2d9 src/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOLCF/IOA/NTP/Receiver.thy	Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Receiver.thy	Thu Jul 17 12:44:58 1997 +0200
@@ -84,6 +84,6 @@
 
 
 receiver_ioa_def "receiver_ioa == 
- (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
+ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
 
 end
diff -r a34c20f4bf44 -r 23eae933c2d9 src/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOLCF/IOA/NTP/Sender.thy	Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Sender.thy	Thu Jul 17 12:44:58 1997 +0200
@@ -80,6 +80,6 @@
       C_r_r(m) => False}"
 
 sender_ioa_def "sender_ioa == 
- (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
+ (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})"
 
 end
diff -r a34c20f4bf44 -r 23eae933c2d9 src/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOLCF/IOA/NTP/Spec.thy	Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Spec.thy	Thu Jul 17 12:44:58 1997 +0200
@@ -37,6 +37,6 @@
       C_r_s => False |                            
       C_r_r(m) => False}"
 
-ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
+ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans,{},{})"
 
 end