#.model resource
#.state st2 = m_st:U
#.state st3 = r_st:I
#.negfair
#.subsets {st2}
#.subsets {st3}
#.endfair
#.endmodel
## TESLA ver 0.2
# assertion 0: req implies (req until grant) then (use until release)
!(m_st=D);
!(r_st=I);