PROMELA WITH SPIN

PROMELA setauku merupakan bahasa permodelan untuk memodelkan kelakuan sebuah proses atau sistem. Biasanya interaksi antara manusia dan komputer, atau komputer dengan komputer itu enaknya di buat modelnya dulu kali yaaa ... lantas gimana dengan hubungan manusia dengan Tuhan, manusia dengan manusia, dan manusia dengan hewan .... perlu kali yaaaa

Tugas Kuliah : Bikin permodelan TFTP menggunakan SPIN ....


Instalasi SPIN, mau make xspin gak? kalo mau make xspin kita harus donwload dulu cygwin, install dan sertakan library c compiler dan tcl interpreter. cygwin bisa di download pada url http://www.cygwin.com/, kemudian lakukan instalasi

duh ... baiknya pelajari dulu dari contoh yang sudah ada. Vending Machine. Vending machine itu kayak mesin penyedia minuman gituh. Minuman yang di sediakan sesuai dengan coin yang di masukkan ke dalam mesin. Jadi misal kalo kita masukin coin 50 maka yang muncul itu teh, kalo kita masukin coin 100 yang muncul coffee. Di indonesia ada gak ya .... mesin beginian ... yang bisa ngeluarin es dawet basi, es cendol basi, Bakso gituhhh, tapi kalo di indonesia mungkin tanpa masukin coin pun udah ngocor sendiri ... hahaha

So let's we start dari deskripsi vending machine di atas maka promela nya bisa seperti ini:

mtype={coin50,coin100,tea,coffee}
chan coin_channel = [1] of {mtype}
chan drinks_channel = [1] of {mtype}

proctype customer {
if
:: coin_channel!coin50;drinks_channel?tea;
:: coin_channel!coin100;drinks_channel?coffee;
fi
}

proctype vender {
if
::coin_channel?coin50;drinks_channel!tea;
::coin_channel?coin100;drinks_channel!coffee;
fi
}

init{run customer;run vender;}

Kira kira promela di atas itu kalo di bahasa indonesiakan gini kali ya :

1. customer masukin coin5o => coin_channel!coin50
2. vending machine menerima coin50 => coin_channel?coin50
3. vending machine mengirim tea => drinks_channel!tea
4. customer menerima tea => drinks_channel?tea

sampe sini sih paham .... tapi tugas aku itu TFTP , trivial file transfer protocol, jadi harus baca dulu dokumen rfc 1350. Intinya sih simple ya ada dua proses yaitu WRQ dan RRQ

WRQ (Write Request)
Client mengirimkan wrq ke server , jika server mengizinkan maka server akan membalas nya dengan ack0, client kemudian akan membalasnya dengan mengirim data0, kemudian server mengirimkan ack1 yang artinya client bisa mengirimkan data1

RRQ(Read Request)
Bedanya dengan WRQ, jika client mengirimkan RRQ maka server akan langsung memberikan data0

Kira kira begitu .... nah gimana sekarang promela nya ... yang sederhana aja ah, kalo yang mendekati real komunikasi FTP nanti tanya ama mas yazid aja ... sekarang yang kira kira aja ....
loading dulu ...ahhhh

Wah waktunya gak cukup buat loading terlalu lama, FSM nya gak kebayang .... daripada gak ngumpul tugas nih hahahha mendingan aku bikin kayak gini aja :

RRQ nya jadi kayak gini

Karena aku lom berhasil instalasi xspin , sebab install cygwin aja gagal terus ya terpaksa gak pake xspin

mtype = {DATA0,DATA1,RRQ,ACK0,ACK1,DATAreq}
chan ch_rrq = [1] of {mtype}; chan ch_data = [1] of {mtype}; chan ch_status = [1] of {mtype}; chan SAP1 = [1] of {mtype}; proctype client() {
byte state;
do
::SAP1?DATAreq;ch_rrq!RRQ;
if
::ch_data?DATA0;ch_status!ACK0; ::ch_data?DATA1;ch_status!ACK1;
fi
od
}

proctype server() {
do ::ch_rrq?RRQ->ch_data!DATA0;
if
::ch_status?ACK0 -> ch_data!DATA1;
::ch_status?ACK1 -> ch_data!DATA0;
fi
od
}

proctype user() {
byte n=0;
do
::(n <>SAP1!DATAreq;n=n+1
::n==10->break
od
}

init {run user();run client();run server();}


WRQ nya jadi kayak gini :

mtype = {DATA0,DATA1,WRQ,ACK0,ACK1,DATAupload}
chan ch_wrq = [1] of {mtype};
chan ch_data = [1] of {mtype};
chan ch_status = [1] of {mtype};
chan SAP1 = [1] of {mtype};
proctype client() {
byte state;
do
::SAP1?DATAupload;ch_wrq!WRQ;
if
::ch_status?ACK0;ch_data!DATA0;
::ch_status?ACK1;ch_data!DATA1;
fi
od
}

proctype server() {
do
::ch_wrq?WRQ->ch_status!ACK0;
if
::ch_data?DATA0 -> ch_status!ACK1;
::ch_data?DATA1 -> ch_status!ACK0;
fi
od
}

proctype user() {
byte n=0;
do
::(n <>SAP1!DATAupload;n=n+1
::n==10->break
od
}

init {run user();run client();run server();}

Benar tidaknya gak tau nih ... setidaknya aku sudah mencoba ... nanti kita minta punya mr yazid gimana ......
BAKAAAAAAAAAAAAAAAAAAAAAAA