[Pntool-developers] SF.net SVN: pntool:[258] present_version/examples
Brought to you by:
compaqdrew,
miordache
Menu
▾
▴
[Pntool-developers] SF.net SVN: pntool:[258] present_version/examples
|
From: <mio...@us...> - 2011-07-28 16:39:31
|
Revision: 258
http://pntool.svn.sourceforge.net/pntool/?rev=258&view=rev
Author: miordache
Date: 2011-07-28 16:39:24 +0000 (Thu, 28 Jul 2011)
Log Message:
-----------
more examples
Modified Paths:
--------------
present_version/examples/README
Added Paths:
-----------
present_version/examples/test2.sp
present_version/examples/test3a.sp
present_version/examples/test3c.sp
present_version/examples/test3d.sp
Modified: present_version/examples/README
===================================================================
--- present_version/examples/README 2011-07-28 15:06:37 UTC (rev 257)
+++ present_version/examples/README 2011-07-28 16:39:24 UTC (rev 258)
@@ -2,3 +2,17 @@
inteq.sp: a simple example illustrating how to write concurrent program specifications. It specifies a concurrent program for finding integer solutions to the equation w^2 = x^2 + y^2 + z^2.
+
+The following files were converted to the present specification format by Micah Martin and Basil Hall.
+
+test2.sp: This is a test file intended to check the code generation module. It generates a process that can creates periodically a thread until it terminates. There are synchronizations between the process and the threads it generates.
+
+
+
+test3: A dining philosopher example.
+
+test3a.sp: Tests that the deadlock prevention function works fine when no deadlock is possible. Only one philosopher with two resources.
+
+test3c.sp: A test involving 5 philosophers.
+
+test3d.sp: A test involving 5 philosophers. Here, the resources (chopsticks) are defined as supervisor components, not as threads.
Added: present_version/examples/test2.sp
===================================================================
--- present_version/examples/test2.sp (rev 0)
+++ present_version/examples/test2.sp 2011-07-28 16:39:24 UTC (rev 258)
@@ -0,0 +1,114 @@
+// This is a test file intended to check the code generation module
+// The example of this file was adapted from compexample.c
+
+process TYPE1 {
+
+ places: p0 p1 p2
+ transitions: t0 t1 t2 t3 t4
+
+ // Let's create the following PN:
+ //
+ // t2
+ // -------|<----
+ // | p0 p1 |p2
+ // ->O->|->O->|->O<--
+ // | t0 | t1 |
+ // | | |
+ // | V |
+ // | --- t3 |
+ // | |
+ // ------>|-------
+ // t4
+
+ (p0, t4, p2)
+ (p1, t3)
+ (p2, t2, p0)
+ (p1, t1, p2)
+ (p0, t0, p1)
+}
+
+thread PN3 {
+
+ places: p0 p1
+ transitions: t0 t1 t2
+
+ // Let's create this PN:
+ //
+ // p0 p1
+ // |->O->|->O->|
+ // t2 t0 t1
+ //
+
+ (t2, p0)
+ (p0, t0, p1)
+ (p1, t1)
+}
+
+initialize: TYPE1(p0:1)
+initialize: PN3(p0:0)
+
+TYPE1.p0 {
+ u++;
+ fprintf(stderr, "\nPN: State 0 u = %d", u);
+ delay(1);
+}
+
+TYPE1.p1 {
+ fprintf(stderr, "\nPN: State 1");
+ delay(1);
+}
+
+TYPE1.p2 {
+ fprintf(stderr, "\nPN: State 2");
+ delay(1);
+}
+
+PN3.p0 {
+ u++;
+ printf("\nPN3: State 0 u = %d", u);
+ delay(2);
+}
+
+PN3.p1 {
+ printf("\nPN3: State 1");
+ delay(2);
+}
+
+TYPE1.include {
+ #include<stdio.h>
+ int pr1_state = 0, i, j, u = 0;
+
+ void delay(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+
+ int f1(int z) {
+ struct ___trans ___TR[1];
+ if(u > 5) {
+ ___TR[0].no_output = 1;
+ ___TR[0].label = -4;
+ ___TR[0].trans = 3;
+ }
+ else {
+ ___TR[0].no_output = 0;
+ ___TR[0].label = -2;
+ ___TR[0].trans = 1;
+ ___TR[0].place = 2;
+ }
+ return 1;
+ }
+}
+
+PN3.include {
+ #include<stdio.h>
+ int pr1_state = 0, i, j, u = 0;
+
+ void delay(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+TYPE1.build {gcc -g -o $$$.exe $$$.c }
+
Added: present_version/examples/test3a.sp
===================================================================
--- present_version/examples/test3a.sp (rev 0)
+++ present_version/examples/test3a.sp 2011-07-28 16:39:24 UTC (rev 258)
@@ -0,0 +1,91 @@
+// This is a test file intended to check the code generation module
+
+thread ph1 {
+
+ places: p0 p1 p2 p3
+ transitions: t0 t1 t2 t3 t4
+
+ // t3
+ // ------------|<---------------
+ // | |
+ // ->O-->|-->O-->|-->O-->|-->O--
+ // p0 t0 p1 t1 p2 t2 p3
+
+ (p0, t0, p1); (p1, t1, p2); (p2, t2, p3); (p3, t3, p0)
+}
+
+thread left {
+
+ places: p
+ transitions: t0 t2
+
+ // --->| t2
+ // p |
+ // t0 |--->O
+ //
+
+ (p, t2); (t0, p)
+}
+
+initialize: left(p:1) ph1(p0:1)
+
+live: ph1.t1
+
+ph1.p0 {
+ u++;
+ fprintf(stderr, "\nPhil. State 0 (think) u = %d", u);
+ fflush(0);
+ delay(1);
+}
+
+ph1.p1 {
+ fprintf(stderr, "\nPN: State 1 (requesting right fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p2 {
+ fprintf(stderr, "\nPN: State 2 (requesting left fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p3 {
+ fprintf(stderr, "\nPN: State 3 (eat)");
+ fflush(0);
+ delay(1);
+}
+
+left.p {
+ fprintf(stderr, "\nResource %s is available", ___NAME);
+ fflush(0);
+}
+
+ph1.include {
+ #include<stdio.h>
+ int pr1_state = 0, i, j, u = 0;
+
+ void delay(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+left.include {
+ #include<stdio.h>
+ static int v = 0;
+
+ static void delay2(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+right = left // right is a copy of the thread left
+
+initialize: right(p:1) //the assignment above does not copy the initial marking
+
+sync ph1.t1 left.t2
+sync ph1.t2 right.t2
+sync ph1.t3 left.t0
+sync ph1.t3 right.t0
Added: present_version/examples/test3c.sp
===================================================================
--- present_version/examples/test3c.sp (rev 0)
+++ present_version/examples/test3c.sp 2011-07-28 16:39:24 UTC (rev 258)
@@ -0,0 +1,107 @@
+// This is a test file intended to check the code generation module
+
+thread ph1 {
+
+ places: p0 p1 p2 p3
+ transitions: t0 t1 t2 t3 t4
+
+ // t3
+ // ------------|<---------------
+ // | |
+ // ->O-->|-->O-->|-->O-->|-->O--
+ // p0 t0 p1 t1 p2 t2 p3
+
+ (p0, t0, p1); (p1, t1, p2); (p2, t2, p3); (p3, t3, p0)
+}
+
+thread r1 {
+
+ places: p
+ transitions: t0 t1 t2 t3
+
+ // --->| t2
+ // p |
+ // t0 |--->O<---| t1
+ // |
+ // --->| t3
+
+ (p, t2); (p, t3); (t0, p); (t1, p)
+}
+
+initialize: r1(p:1) ph1(p0:1)
+
+ph1.p0 {
+ u++;
+ fprintf(stderr, "\nPhil. State 0 (think) u = %d", u);
+ fflush(0);
+ delay(1);
+}
+
+ph1.p1 {
+ fprintf(stderr, "\nPN: State 1 (requesting right fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p2 {
+ fprintf(stderr, "\nPN: State 2 (requesting left fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p3 {
+ fprintf(stderr, "\nPN: State 3 (eat)");
+ fflush(0);
+ delay(1);
+}
+
+r1.p {
+ fprintf(stderr, "\nResource %s is available", ___NAME);
+ fflush(0);
+}
+
+ph1.include {
+ #include<stdio.h>
+ static int pr1_state = 0, i, j, u = 0;
+
+ static void delay(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+r1.include {
+ #include<stdio.h>
+ static int v = 0;
+
+ static void delay2(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+r2 = r1
+r3 = r1
+r4 = r1
+r5 = r1
+
+ph2 = ph1
+ph3 = ph1
+ph4 = ph1
+ph5 = ph1
+
+
+initialize: r2(p:1) ph2(p0:1) r3(p:1) ph3(p0:1) r4(p:1) ph4(p0:1) r5(p:1) ph5(p0:1)
+
+
+sync ph1.t1 r1.t2; sync ph2.t1 r2.t2; sync ph3.t1 r3.t2; sync ph4.t1 r4.t2; sync ph5.t1 r5.t2
+
+sync ph1.t2 r5.t3; sync ph2.t2 r1.t3; sync ph3.t2 r2.t3; sync ph4.t2 r3.t3; sync ph5.t2 r4.t3
+
+sync ph1.t3 r1.t0 r5.t1; sync ph2.t3 r2.t0 r1.t1; sync ph3.t3 r3.t0 r2.t1; sync ph4.t3 r4.t0 r3.t1; sync ph5.t3 r5.t0 r4.t1
+
+live: ph1.t1
+live: ph2.t1
+live: ph3.t1
+live: ph4.t1
+live: ph5.t1
Added: present_version/examples/test3d.sp
===================================================================
--- present_version/examples/test3d.sp (rev 0)
+++ present_version/examples/test3d.sp 2011-07-28 16:39:24 UTC (rev 258)
@@ -0,0 +1,91 @@
+// This is a test file intended to check the code generation module
+
+thread ph1 {
+
+ places: p0 p1 p2 p3
+ transitions: t0 t1 t2 t3 t4
+
+ // t3
+ // ------------|<---------------
+ // | |
+ // ->O-->|-->O-->|-->O-->|-->O--
+ // p0 t0 p1 t1 p2 t2 p3
+
+ (p0, t0, p1); (p1, t1, p2); (p2, t2, p3); (p3, t3, p0)
+}
+
+supervisor r1 {
+
+ places: p
+ transitions: t0 t1 t2 t3
+
+ // --->| t2
+ // p |
+ // t0 |--->O<---| t1
+ // |
+ // --->| t3
+
+ (p, t2); (p, t3); (t0, p); (t1, p)
+}
+
+initialize: r1(p:1) ph1(p0:1)
+
+ph1.p0 {
+ u++;
+ fprintf(stderr, "\nPhil. State 0 (think) u = %d", u);
+ fflush(0);
+ delay(1);
+}
+
+ph1.p1 {
+ fprintf(stderr, "\nPN: State 1 (requesting right fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p2 {
+ fprintf(stderr, "\nPN: State 2 (requesting left fork)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.p3 {
+ fprintf(stderr, "\nPN: State 3 (eat)");
+ fflush(0);
+ delay(1);
+}
+
+ph1.include {
+ #include<stdio.h>
+ static int pr1_state = 0, i, j, u = 0;
+
+ static void delay(int n) {
+ time_t a, b;
+ for(time(&a), time(&b); a + n > b; time(&b));
+ }
+}
+
+
+r2 = r1
+r3 = r1
+r4 = r1
+r5 = r1
+
+ph2 = ph1
+ph3 = ph1
+ph4 = ph1
+ph5 = ph1
+
+initialize: r2(p:1) ph2(p0:1) r3(p:1) ph3(p0:1) r4(p:1) ph4(p0:1) r5(p:1) ph5(p0:1)
+
+sync ph1.t1 r1.t2; sync ph2.t1 r2.t2; sync ph3.t1 r3.t2; sync ph4.t1 r4.t2; sync ph5.t1 r5.t2
+
+sync ph1.t2 r5.t3; sync ph2.t2 r1.t3; sync ph3.t2 r2.t3; sync ph4.t2 r3.t3; sync ph5.t2 r4.t3
+
+sync ph1.t3 r1.t0 r5.t1; sync ph2.t3 r2.t0 r1.t1; sync ph3.t3 r3.t0 r2.t1; sync ph4.t3 r4.t0 r3.t1; sync ph5.t3 r5.t0 r4.t1
+
+live: ph1.t1
+live: ph2.t1
+live: ph3.t1
+live: ph4.t1
+live: ph5.t1
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
