#.model system
#.state st0 = st_perm0:1
#.state st1 = st_perm1:1
#.negfair
#.subsets{st0}
#.subsets{st1}
#.endfair
#.endmodel
!(st_perm0=1);
!(st_perm1=1);

#.model process
#.state critical_section = pc:L12
#.state soso_section = pc:L16
#.negfair
#.subsets{critical_section}
#.subsets{soso_section}
#.endfair
#.endmodel
!(p0.pc=L12);
!(p0.pc=L16);
!(p1.pc=L12);
!(p1.pc=L16);