Require Export SFSstate.

Section setACLdata.

Variable s : SFSstate.


Definition ChangeUserR (u : SUBJECT) (x : set SUBJECT)
  (oct : RIGHTS) : set SUBJECT :=
  match oct with
  | allowedTo false false ⇒ set_remove SUBeq_dec u x
  | allowedTo false true ⇒ set_remove SUBeq_dec u x
  | allowedTo true false ⇒ set_add SUBeq_dec u x
  | allowedTo true true ⇒ set_add SUBeq_dec u x
  end.


Definition ChangeUserW (u : SUBJECT) (x : set SUBJECT)
  (oct : RIGHTS) : set SUBJECT :=
  match oct with
  | allowedTo false false ⇒ set_remove SUBeq_dec u x
  | allowedTo false true ⇒ set_add SUBeq_dec u x
  | allowedTo true false ⇒ set_remove SUBeq_dec u x
  | allowedTo true true ⇒ set_add SUBeq_dec u x
  end.


Definition ChangeGroupR (g : GRPNAME) (oct : RIGHTS)
  (x : set GRPNAME) : set GRPNAME :=
  match oct with
  | allowedTo false false ⇒ set_remove GRPeq_dec g x
  | allowedTo false true ⇒ set_remove GRPeq_dec g x
  | allowedTo true false ⇒ set_add GRPeq_dec g x
  | allowedTo true true ⇒ set_add GRPeq_dec g x
  end.

Definition ChangeGroupW (g : GRPNAME) (oct : RIGHTS)
  (x : set GRPNAME) : set GRPNAME :=
  match oct with
  | allowedTo false false ⇒ set_remove GRPeq_dec g x
  | allowedTo false true ⇒ set_add GRPeq_dec g x
  | allowedTo true false ⇒ set_remove GRPeq_dec g x
  | allowedTo true true ⇒ set_add GRPeq_dec g x
  end.

Definition ChangeGroupO (g : GRPNAME) (x : set GRPNAME) :
  set GRPNAME := set_add GRPeq_dec g x.

End setACLdata.