File Access System in LOTOS

The following specification defines a file access system in LOTOS. The style is heavily constraint-oriented. For a description of the original example see:

Jin Sa and Brian C. Warboys. Specifying concurrent object-based systems using combined specification notations. Technical Report UMCS-91-7-2, Department of Computer Science, University of Manchester, Manchester, UK, July 91.

See Incremental requirements specification and the constraint-oriented style in LOTOS for the background to this specification.

specification FileAccessSystem : noexit

  library
    Boolean, NaturalNumber, String, OctetString
  endlib

  type Op is Boolean, NaturalNumber
    sorts Op
    opns
      open, read, write, close, save :  -> Op
      op0, op1, op2, op3 :              -> Op
      Ord :                     Op      -> Nat
      _ eq _, _ ne _ :          Op, Op  -> Bool
    eqns
      forall op1, op2 : Op
	ofsort Nat
	  Ord (open)                    = 0;
	  Ord (read)                    = Succ (Ord (open));
	  Ord (write)                   = Succ (Ord (read));
	  Ord (close)                   = Succ (Ord (write));
	  Ord (save)                    = Succ (Ord (close));
	  Ord (op0)                     = Succ (Ord (save));
	  Ord (op1)                     = Succ (Ord (op0));
	  Ord (op2)                     = Succ (Ord (op1));
	  Ord (op3)                     = Succ (Ord (op2))
	ofsort Bool
	  op1 eq op2                    = Ord (op1) eq Ord (op2);
	  op1 ne op2                    = not (op1 eq op2)
  endtype (* Op *)

  type Dir is NaturalNumber
    sorts Dir
    opns
      inv, ret :                        -> Dir
      Ord :             Dir             -> Nat
      _ eq _, _ ne _ :  Dir, Dir        -> Bool
    eqns
      forall dir1, dir2 : Dir
	ofsort Nat
	  Ord (inv)                     = 0;
	  Ord (ret)                     = Succ (Ord (inv))
	ofsort Bool
	  dir1 eq dir2                  = Ord (dir1) eq Ord (dir2);
	  dir1 ne dir2                  = not (dir1 eq dir2)
  endtype (* Dir *)

  type Orig is NaturalNumber
    sorts Orig
    opns
       t1, t2, app :                    -> Orig
       Ord :            Orig            -> Nat
      _ eq _, _ ne _ :  Orig, Orig      -> Bool
    eqns
      forall orig1, orig2 : Orig
	ofsort Nat
	  Ord (t1)                      = 0;
	  Ord (t2)                      = Succ (Ord (t1));
	  Ord (app)                     = Succ (Ord (t2))
	ofsort Bool
	  orig1 eq orig2                = Ord (orig1) eq Ord (orig2);
	  orig1 ne orig2                = not (orig1 eq orig2)
  endtype (* Orig *)

  type Octs is OctetString
    opns
      _--_ :            OctetString, OctetString        -> OctetString
    eqns
      forall o1, o2 : Octet, os1, os2 : OctetString
	ofsort OctetString
	  <> -- os2                     = <>;
	  os1 -- <>                     = os1;
	  o1 eq o2 =<
	    (o1 + os1) -- (o2 + os2)    = os1 -- os2;
	  o1 ne o2 =<
	    (o1 + os1) -- (o2 + os2)    = <>;
  endtype (* Octs *)

behaviour
  hide fh, t1, t2 in
    Sys [fh, t1, t2]

where

  process Sys [fh, t1, t2] : noexit :=
    SysGen [fh]
  ||
    FH [fh]
  ||
    (
      Appl [fh, t1, t2]
    |[t1, t2]|
      (T1 [fh, t1] ||| T2 [fh, t2])
    )

  where

    process SysGen [fh] : noexit :=
      SysOpen [fh]
    |[fh]|
      SysClose [fh]
    |[fh]|
      SysWrite [fh]

    where

      process SysOpen [fh] : noexit :=
	fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	  [(op eq open) implies (orig eq t1)];
	SysOpen [fh]
      endproc (* SysOpen *)

      process SysClose [fh] : noexit :=
	fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	  [(op eq close) implies (orig eq t1)];
	SysClose [fh]
      endproc (* SysClose *)

      process SysWrite [fh] : noexit :=
	fh ! read ! inv ? octs : OctetString ! t1;
	fh ? op : Op ? dir : Dir ? octs : OctetString ! t1;
	SysWrite1 [fh]
      []
	fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	  [(op ne read) or (dir ne inv) or (orig ne t1)];
	SysWrite [fh]

      where

	process SysWrite1 [fh] : noexit :=
	  fh ! read ! ret ? octs : OctetString ! t1;
	  SysWrite [fh]
	[]
	  fh ? op : Op ? dir : Dir ? octs : OctetString ! t1
	    [(op ne read) or (dir ne ret)];
	  SysWrite1 [fh]
	endproc (* SysWrite1 *)

      endproc (* SysWrite *)

    endproc (* SysGen *)

    process FH [fh] : noexit :=
      FHComm [fh] || FHOper [fh] || FHCall [fh] || FHData [fh]

    where

      process FHComm [fh] : noexit :=
	fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig;
	FHComm [fh]
      endproc (* FHComm *)

      process FHOper [fh] : noexit :=
	FHOpname [fh] || FHOpen [fh] || FHClose [fh] || FHSave [fh]

      where

	process FHOpname [fh] : noexit :=
	  fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig;
	  FHOpname [fh]
	endproc (* FHOpname *)

	process FHOpen [fh] : noexit :=
	  fh ! open ! inv ? octs : OctetString ? orig : Orig;
	  FHOpen1 [fh]

	where

	  process FHOpen1 [fh] : noexit :=
	    fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	      [(op ne open) or (dir ne inv)];
	    FHOpen1 [fh]
	  endproc (* FHOpen1 *)

	endproc (* FHOpen *)

	process FHClose [fh] : noexit :=
	  FHClose1 [fh]
	[>
	  fh ! close ! ret ? octs : OctetString ? orig : Orig;
	  stop

	where

	  process FHClose1 [fh] : noexit :=
	    fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	      [(op ne close) or (dir ne ret)];
	    FHClose1 [fh]
	  endproc (* FHClose1 *)

	endproc (* FHClose *)

	process FHSave [fh] : noexit :=
	  fh ! write ? dir : Dir ? octs : OctetString ? orig : Orig;
	  FHSave1 [fh]
	[]
	  fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	    [op ne write];
	  FHSave [fh]

	where

	  process FHSave1 [fh] : noexit :=
	    fh ! save ? dir : Dir ? octs : OctetString ? orig : Orig;
	    FHSave [fh]
	  []
	    fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
	      [op ne save];
	    FHSave1 [fh]

	  endproc (* FHSave1 *)

	endproc (* FHSave *)

      endproc (* FHOper *)

      process FHCall [fh] : noexit :=
	fh ? op : Op ! inv  ? octs : OctetString ? orig : Orig;
	fh ! op ! ret ? octs : OctetString ! orig;
	FHCall [fh]
      endproc (* FHCall *)

      process FHData [fh] : noexit :=
	FHNotIO [fh] ||| ((FHRead [fh] ||| FHWrite [fh]) || FHFile [fh] (<>))

      where

	process FHNotIO [fh] : noexit :=
	  fh ? op : Op ? dir : Dir ? octs : OctetString
	    [(op ne read) and (op ne write)];
	  FHNotIO [fh]
	endproc (* FHRead *)

	process FHRead [fh] : noexit :=
	  fh ! read ! ret ? octs : OctetString ? orig : Orig;
	  FHRead [fh]
	endproc (* FHRead *)

	process FHWrite [fh] : noexit :=
	  fh ! write ! inv ? octs : OctetString ? orig : Orig [octs ne <>];
	  FHWrite [fh]
	endproc (* FHWrite *)

	process FHFile [fh] (octs : OctetString) : noexit :=
	  fh ! write ! inv ? octs1 : OctetString ? orig : Orig;
	  FHFile [fh] (octs ++ octs1)
	[]
	  fh ! read ! ret ! octs ? orig : Orig;
	  FHFile [fh] (octs)
	endproc (* FHFile *)

      endproc (* FHData *)

    endproc (* FH *)

    process T1 [fh, t1] : noexit :=
      T1Op1 [fh, t1] ||| T1Op2 [fh, t1] ||| T1Op3 [fh, t1]

    where

      process T1Op1 [fh, t1] : noexit :=
	t1 ! op1 ! inv ! <> ! app;
	  fh ! open ! inv ? octs : OctetString ! t1;
	  fh ! open ! ret ? octs : OctetString ! t1;
	t1 ! op1 ! ret ! <> ! app;
	T1Op1 [fh, t1]
      endproc (* T1Op1 *)

      process T1Op2 [fh, t1] : noexit :=
	t1 ! op2 ! inv ? octs1 : OctetString ! app;
	  fh ! read ! inv ? octs : OctetString ! t1;
	  fh ! read ! ret ? octs2 : OctetString ! t1;
	  fh ! write ! inv ! octs1 ! t1;
	  fh ! write ! ret ? octs : OctetString ! t1;
	  fh ! read ! inv ? octs : OctetString ! t1;
	  fh ! read ! ret ? octs3 : OctetString ! t1;
	t1 ! op2 ! ret ! octs3 -- octs2 ! app;
	T1Op2 [fh, t1]
      endproc (* T1Op2 *)

      process T1Op3 [fh, t1] : noexit :=
	t1 ! op3 ! inv ! <> ! app;
	  fh ! close ! inv ? octs : OctetString ! t1;
	  fh ! close ! ret ? octs : OctetString ! t1;
	t1 ! op3 ! ret ! <> ! app;
	T1Op3 [fh, t1]
      endproc (* T1Op3 *)

    endproc (* T1 *)

    process T2 [fh, t2] : noexit :=
      t2 ! op0 ! inv ? octs : OctetString ! app;
	fh ! write ! inv ! octs ! t2;
	fh ! write ! ret ? octs : OctetString ! t2;
      t2 ! op0 ! ret ! <> ! app;
      T2 [fh, t2]
    endproc (* T2 *)

    process Appl [fh, t1, t2] : noexit :=
      fh ? op : Op ? dir : Dir ? octs : OctetString ! app;
      Appl [fh, t1, t2]
    []
      t1 ? op : Op ? dir : Dir ? octs : OctetString ! app;
      Appl [fh, t1, t2]
    []
      t2 ? op : Op ? dir : Dir ? octs : OctetString ! app;
      Appl [fh, t1, t2]
    endproc (* Appl *)

  endproc (* Sys *)

endspec (* FileAccessSystem *)

Up one level to University of Stirling - LOTOS Activities

Web Ken Turner Home   Email    Search Search Web Pages


URL: http://www.cs.stir.ac.uk/well/fas.html