Я создал 4 вида (Task, Role, User и Run), последний получает 2 параметра, затем я объявляю забаву для каждого из них, в том числе один для Run , вызываю P, который получает 2 параметра для создания «экземпляра» Run . Затем я создал два массива, один из которых содержит «отношение» роли пользователя (Privs), а другой — «отношение» роли-задачи (роли). Я использую эти два массива, чтобы утверждать, что при поиске пользователя u у него есть роль r в Privs, и если при поиске роли r в Roles у него есть задача t. До сих пор мне удается делать это отдельными строками, например:
(declare-sort Task)
(declare-sort Role)
(declare-sort User)
(declare-sort Run 2)
(define-sort P (User Role) (Run User Role))
(declare-fun t () Task)
(declare-fun r () Role)
(declare-fun u () User)
(declare-const Privs (Array User Role))
(declare-const Roles (Array Role Task))
(assert (= (select Privs u) r))
(assert (= (select Roles r) t))
Но теперь я пытаюсь сделать забаву, которая получает пару Run (User, Role) и внутри функции утверждает то же самое, но для всех пользователей в P и всех его ролях. Можно ли это сделать, передав в функцию переменную сортировки Run??.. для доступа к ее элементам (User, Role) внутри??
