[Rodin-b-sharp-user] Rodin Set question

[Samah H. <sa...@ya...>]

Dear all,

I am trying to write a model for a motor and a shaft, which both had a state 
idle, it seems that RODIN does not accept that a constant belongs to two 
different sets
it gives the following errors:
 
Type unKnown
Types set1 and set2 does not match

below is the context file 

contextctx1constantsclockwisecounterclockwiseup
 setsset2 
axioms@axm3clockwise≠ idle
@axm4 counterclockwise ≠ idle@axm5set1= {up, down, idle}@axm6 up≠ down@axm7 up≠ 
idle@axm8 down≠ idle　
 
Any suggestions on how to resolve that error and keep the model as it is?
 
Thanks,
Samah
 
 end@axm1set2= {clockwise , counterclockwise , idle 
}@axm2 clockwise≠ counterclockwise set1
downidle