system filesystem;

const NUSERS = 2;
const NFILES = 3;       

type UserIdType = range 0 .. NUSERS;
type FileIdType = range 0 .. NFILES;
type FileStatusType = enum
  Closed, Reading, Writing
endenum;
type ResponseType = enum
  AcceptCommand, RejectCommand
endenum;
type ReasonType = enum
  FileOpenForRead, FileOpenForWrite, FileLocked, FileClosed, FileStatusUnchanged
endenum;

signal openForRead(FileIdType, UserIdType);
signal openForWrite(FileIdType, UserIdType);
signal close(FileIdType, UserIdType);
signal answer(ResponseType, ReasonType);


/* 
 * User Process 
 *
 */

process user(NUSERS);

var f FileIdType;
var response ResponseType;
var reason ReasonType;

state idle #start ;
    output openForRead(f, ({integer}self)) to ({filesys}0);
      nextstate wait_answer;
    output openForWrite(f, ({integer}self)) to ({filesys}0);
      nextstate wait_answer;
    output close(f, ({integer}self)) to ({filesys}0);
      nextstate wait_answer;
    task f := (f + 1) % NFILES;
      nextstate idle; 
endstate;
state wait_answer;
  input answer(response, reason);
    nextstate idle;
endstate;
endprocess;

/*
 * File System Process
 *
 */

process filesys(1);

type FileControlBlockType = array [NUSERS] of FileStatusType;
type SystemStatusType = array [NFILES] of FileControlBlockType;

var f FileIdType;
var u UserIdType;
var response ResponseType;
var reason ReasonType;
var systemStatus SystemStatusType;
var available boolean;

procedure File_Available_For_Read;
  fpar in f FileIdType, in u UserIdType, in systemStatus SystemStatusType;
  returns boolean;
{#
  /* files are always available for reading */
  return 1; 
#}
endprocedure;

procedure File_Available_For_Write;
  fpar in f FileIdType, in u UserIdType, in systemStatus SystemStatusType;
  returns boolean;
{#
  /* true if nobody is updating, maybe except u */
  int uprime ;
  int result=1;
  for (uprime=0; uprime<if_NUSERS_constant; uprime++)
    result &= (uprime==u || systemStatus[f][uprime] != if_Writing_constant);
  return result;
#}
endprocedure;


state start #start ;
    task f := 0;
    while (f < NFILES) do
      task u := 0;
      while (u < NUSERS) do
        task systemStatus[f][u] := Closed;
        task u := (u + 1);
      endwhile
      task f := (f + 1);
    endwhile
    nextstate idle;
endstate;

state idle;
  input close(f, u);
    task response := AcceptCommand;
    if (systemStatus[f][u] <> Closed) then
      task reason := FileClosed;
      task systemStatus[f][u] := Closed;
    else
      task reason := FileStatusUnchanged;
    endif
    output answer(response, reason) to ({user}u);
    nextstate idle;
  input openForRead(f, u);
    if ((systemStatus[f][u] = Reading) or 
        (systemStatus[f][u] = Writing)) then
      task response := AcceptCommand;
      task reason := FileStatusUnchanged;
    else
      available := call File_Available_For_Read(f,u,systemStatus);
      if available then
        task response := AcceptCommand;
        task reason := FileOpenForRead;
        task systemStatus[f][u] := Reading;
      else
        task response := RejectCommand;
        task reason := FileLocked;
      endif
    endif
    output answer(response, reason) to ({user}u);
    nextstate idle;
  input openForWrite(f, u);
    if (systemStatus[f][u] = Writing) then
      task response := AcceptCommand;
      task reason := FileStatusUnchanged;
    else
      available := call File_Available_For_Write(f,u,systemStatus);
      if available then
        task response := AcceptCommand;
        task reason := FileOpenForWrite;
        task systemStatus[f][u] := Writing;
      else
        task response := RejectCommand;
        task reason := FileLocked;
      endif
    endif
    output answer(response, reason) to ({user}u);
    nextstate idle;
endstate;
endprocess;
endsystem;