AstraVer Toolset » Дополнительные материалы к монографии

Сейчас так:

  event delete_user
    any user subject 
    where
      @grd1 user ∈ UserAccs
      @grd2 subject ∈ Subjects
      @grd3 ∀s · s ∈ Subjects ⇒ SubjectUser(s) ≠ user
    then
      @act1 CurrUnion ≔ CurrUnion ∖ {user}
      @act2 UserAccs ≔ UserAccs ∖ {user}
  end

Должно быть так:

  event delete_user
    any user 
    where
      @grd1 user ∈ UserAccs
      @grd2 ∀s · s ∈ Subjects ⇒ SubjectUser(s) ≠ user
    then
      @act1 CurrUnion ≔ CurrUnion ∖ {user}
      @act2 UserAccs ≔ UserAccs ∖ {user}
  end

Листинг 7.6 нужно поправить так:

@event 
def delete_user(user): 
   global CurrUnion
   global UserAccs

   assert user in UserAccs, "grd1" 
   assert all(map(lambda s: SubjectUser[s] != user, Subjects)), "grd2" 

   CurrUnion.discard(user) 
   UserAccs.discard(user)