Mercurial > hg > Members > nobuyasu > Spin

diff Samples/p347.pres.sim.h @ 0:86e67be8bc5f draft

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some files
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Fri, 29 Jun 2012 01:14:43 +0900
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Samples/p347.pres.sim.h	Fri Jun 29 01:14:43 2012 +0900
@@ -0,0 +1,23 @@
+/*
+ * PROMELA Validation Model
+ * Presentation & User Layer - combined and reduced
+ */
+
+proctype present(bit n)
+{	byte status;
+progress0:
+	pres_to_ses[n]!transfer ->
+	do
+	:: pres_to_ses[n]!abort;
+progress1:	skip
+	:: ses_to_pres[n]?accept,status ->
+			break
+	:: ses_to_pres[n]?reject,status ->
+		if
+		:: (status == NON_FATAL) ->
+			goto progress0
+		:: (status != NON_FATAL) ->
+			break
+		fi
+	od
+}