Project

General

Profile

Bug #9299

Глава 7. Поправить пример delete_user

Added by Denis Efremov 6 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Normal
Assignee:
Start date:
10/04/2018
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

Убрать из листинга не используемый параментр subject. Поправить как в Event-B, так и в трансляции на python.

History

#1 Updated by Denis Efremov 5 months ago

Сейчас так:

  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) 

#2 Updated by Ilya Shchepetkov 5 months ago

  • Status changed from New to Closed

Also available in: Atom PDF