// stable marriage uncoord instance // gxn 17/04/10 #const N# dtmc //------------------------------------------------------ // PREFERENCE LISTS // man i prefers woman j over woman k if mij>mik // woman i prefers man j over man k if wij>wik // preference list for men #for i=1:N# #for j=1:N# const int m#i##j#=#N-mod((N-1)-((j-1)-i),N)#; #end# #end# // preference list for women #for i=1:N# #for j=1:N# const int w#i##j#=#mod((N-1)-((i-1)-j),N)+1#; #end# #end# //------------------------------------------------------ // constants used in renaming #for i=1:N# const int N#i#=#i#; #end# //------------------------------------------------------ // module for first man module man1 // current preferences (0 means no preference) m1 : [0..#N#]; // man 1 wants to change #for i=1:N# [e1#i#] m1=0 | #| j=1:N#(m1=#j# & m1#i#>m1#j#)#end# -> (m1'=#i#); #end# // one of the other pairs change so may need to reset its choice #for i=1:N# #for j=2:N# [e#j##i#] true -> (m1'=(m1=#i#)?0:m1); #end# #end# endmodule // construct further men through renaming #for i=2:N# module man#i#=man1[m1=m#i#, #, j=1:N# m1#j#=m#i##j#, #, k=1:N# e#j##k#=e#mod(j-1+i-1,N)+1##k# #end##end# ] endmodule #end# //------------------------------------------------------ // module for first woman module woman1 // do not need a preference (can work it out from the men's preference) // man 1 wants to change #for i=1:N# [e#i#1] (#& j=1:N# m#j#!=N1 #end#) | #| j=1:N#(m#j#=N1 & w1#i#>w1#j#)#end# -> true; #end# endmodule // construct further women through renaming #for i=2:N# module woman#i#=woman1[ N1=N#i#, #, j=1:N# w1#j#=w#i##j#, #, k=1:N# e#k##j#=e#k##mod(j-1+i-1,N)+1# #end##end# ] endmodule #end# //------------------------------------------------------ // initial states: all complete matching init #& i=1:N##& j=i+1:N# m#i#!=m#j# #end# #end# // each man is matched to a diiferent woman #& i=1:N# m#i#>0 #end# // all men are matched endinit //------------------------------------------------------ // reward structure: expected steps rewards "rounds" true : 1; endrewards