Я новичок в OCL и в настоящее время пытаюсь выяснить, как делать инварианты.
Я приложил картинку с диаграммой, над которой я работаю.
https://imgur.com/1ucZq5w
инварианты, которые я пытаюсь разрешить:
a) У игрока на руках 0 или 2 карты.
Context Player
inv i1: self.card->size()=0 or self.card->size()=2
b) Игрок, не сыгравший ни одного раунда, не может иметь больше игрового капитала, чем максимальный бай-ин стола.
Context Player
inv i2: self.numberOfRounds=0 implies (self.gameCapital < self.Table.maxBuyIn)
в) За каждым столом могут находиться только игроки, принадлежащие разным пользователям
Context Player
inv i3: Player.UserAccount.allInstances().userID->isUnique()
Я не уверен, что allInstances () должен идти после Player или после PlayerAccount.
И я не знаю, что я должен делать с частью текста «У каждого стола».
Есть еще два момента, которые я действительно не знаю, как это сделать.
г) В колоде 52 карты, которые отличаются друг от друга по цвету или значению
e) Входные данные всех игроков, у которых все еще есть карты в руке, равны, когда bidDone True.
Подскажите, пожалуйста, правильно ли то, что я сделал до сих пор, и, возможно, какой-нибудь совет или решение для d) и e)?
Любая помощь приветствуется!