--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p337.fserver.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,29 @@
+/*
+ * File Server Validation Model
+ */
+
+proctype fserver(bit n)
+{
+end:	do
+	:: ses_to_fsrv[n]?create ->	/* incoming */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: ses_to_fsrv[n]?data
+			:: ses_to_fsrv[n]?eof -> break
+			:: ses_to_fsrv[n]?close -> break
+			od
+		fi
+	:: ses_to_fsrv[n]?open ->		/* outgoing */
+		if
+		:: fsrv_to_ses[n]!reject
+		:: fsrv_to_ses[n]!accept ->
+			do
+			:: fsrv_to_ses[n]!data -> progress: skip
+			:: ses_to_fsrv[n]?close -> break
+			:: fsrv_to_ses[n]!eof -> break
+			od
+		fi
+	od
+}