annotate Samples/App.F.pftp.pml @ 2:a2dac3fa7383 draft default tip

add Makefile
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Fri, 29 Jun 2012 06:22:47 +0900
parents 86e67be8bc5f
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 /*
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 * PROMELA Validation Model - startup script
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 */
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 #include "App.F.defines.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 #include "App.F.user.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 #include "App.F.present.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 #include "App.F.session.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 #include "App.F.fserver.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 #include "App.F.flow_cl.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 #include "App.F.datalink.h"
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 init
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 { atomic {
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 run userprc(0); run userprc(1);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 run present(0); run present(1);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 run session(0); run session(1);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 run fserver(0); run fserver(1);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 run fc(0); run fc(1);
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 run data_link()
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 }
86e67be8bc5f add some files
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 }