Model FSA { Node alphabet[1]{ size : int; minSize : $self.size>0$ } Node State { name : String {id}; ins : State[*]; outs : State[*]; initial: boolean = false; final : boolean = false; determ1 : $self.Transitionouts.collect( t | t.symbol).asSet().size()=self.Transitionouts.size()$ // non-repeated symbols determ2 : $alphabet.exists( a | a.size= self.Transitionouts.size())$ determ3 : $alphabet.exists( a | self.Transitionouts.forAll( t | t.symbol