asked on

Finite state process

hello
i need some help construcing a fsp model in Labelled Transition System Analyzer.

i want to model a p2p file sharing system

o      create – adds an entry in the local buffer
o      read – accesses a local/remote file
o      write – an exclusive operation and modifies a local/remote file
o      delete – an exclusive operation and deletes a local/remote file
o      dir – displays all local files
o      rdir – displays all remote files

at the moment i can only hand draw the model for this but i cant devise code for it.

im not asking anyone to do this. i only want someone to direct me to a website where i can improve my skills using LTSA

any help will be great

thankyou

ASKER CERTIFIED SOLUTION

sreenathk

membership

This solution is only available to members.

To access this solution, you must be a member of Experts Exchange.

Start Free Trial

isarasoo

ASKER

hello i have derived a some code to perform some the actions however i cant get one peer to view the other peers files.
i.e. when peer "a" hits rdir it should give you options available to peer "b".
heres my code so far its written in LTSA i need help on the RDIR function

const Max =1
range Int =0..Max

SEMAPHORE(N=0) = SEMA[N],
SEMA[v:Int] = (up ->SEMA[v+1] | when(v>0) down-> SEMA[v-1]),
SEMA[Max+1] = ERROR.

BUFFER(N=2)= SLOTS[0],
SLOTS[i:0..N] = (when(i>=0 && i<N)create-> SLOTS[i+1]
                  |when(i>0) d.down ->delete-> d.up->SLOTS[i-1]
                  |when(i>0) read -> SLOTS[i]
                  |when(i>0) w.down ->write -> w.up -> SLOTS[i]
                  |when(i>0) dir -> SLOTS[i]
                  |when(i>0) rdir-> SLOTS[i]).

CREATE = (create -> CREATE).
DELETE=(delete->DELETE).
||D =(DELETE || w:SEMAPHORE(1)).
WRITE = (write->WRITE).
||W = (WRITE || w:SEMAPHORE(1)).
READ = (read -> READ).
DIR =(dir -> DIR).
RDIR = (rdir ->RDIR).

||P2P = (a:BUFFER(2) ||b:BUFFER(2)).

jjames4

please can some explain this code for me please