library CaseStudies/PuCache/PFS_Protocol

from Basic/StructuredDatatypes get List
from Basic/CharactersAndStrings get String
from CaseStudies/Misc/Prerequisites get Prerequisites

spec PFS_Protocol =
  String and Prerequisites
and
  List[sort ExtAttribute fit sort Elem |-> ExtAttribute]
        with List[ExtAttribute] |-> ExtAttributes
then

%% Simplified version of the PFS_Protocol for verification of PuCache

sort OfflineList, Filehandle, Ptr;
op nullPtr:Ptr;

free type FType ::= FTypeUndef | Reg | Dir | Lnk | Sock | Fifo

free type Data ::= Data (Ptr)

free type Time ::= Time (seconds     : Int;
                  nanoSeconds : Int)

free type Attributes ::= Attr (fType : FType; mode : Mode;   nLink  : Int;
                        uid   : Uid;   gid  : Gid;    size   : Size;
                        used  : Size;  fsId : Int; fileId : FileId;
                        atime : Time; mtime : Time;   ctime  : Time)

op
 emptyAttributes : Attributes;

forall a:Attributes
. emptyAttributes = Attr(FTypeUndef, 0, 0, 0, 0, 0, 0, 0, 0, Time(0, 0), Time(0, 0), Time(0, 0))

%% Uid und Gid sind jetzt eigentlich Strings!!!!

free type ExtAttribute ::= ExtAttr (name : String;
                             val  : String)


free type PFS_Answer ::= GetMTime(time:?Time)
                         | Read (attr:?Attributes; count:?Count; eof:?Boolean;
                                 data:?Data)

free type PFS_Return ::= Ret (err    : Errno;
                       retval : PFS_Answer)


%% and lots more - originally


free type PFS_Command ::= GetMTimeArg (fh:Filehandle)
                          | ReadArg (fh:Filehandle; off:?Offset; cnt:?Count)

free type PFS_Request ::= Req (user : Uid;
                        req  : PFS_Command)


%% and lots more - originally

preds
  __>=__ : Time * Time;

ops
 __>=__ : Time * Time -> Boolean;

forall t1,t2:Time
. t1 >= t2 <=> seconds(t1) > seconds(t2)
        \/ (seconds(t1) = seconds(t2) /\ nanoSeconds(t1) >= nanoSeconds(t2))
. (t1>=t2) = True when (t1>=t2) else False