```// 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
```