Skip to content

GitLab

Commit 41d0d5a6 authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Fix GIOP models

parent 174a304c
Hide whitespace changes
Inline Side-by-side
Showing with 66 additions and 55 deletions
tests/case_studies/giop/giop1.nomig.pr
View file @ 41d0d5a6
......@@ -10,6 +10,11 @@
* Copyright (C) 1998 by Moataz Kamel. All rights reserved.
*****************************************************************************/
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define CHANLEN 5 /* default channel length (5) */
#define MAXREQID 4 /* maximum number for request_id (4) */
#define NUMOBJS 2 /* number of objects (2) */
......
tests/case_studies/giop/giop2.nomig.pr
View file @ 41d0d5a6
......@@ -9,7 +9,11 @@
*
* Copyright (C) 1998 by Moataz Kamel. All rights reserved.
*****************************************************************************/
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
#define CHANLEN 5 /* default channel length (5) */
#define MAXREQID 4 /* maximum number for request_id (4) */
#define NUMOBJS 2 /* number of objects (2) */
......
tests/case_studies/giop/giop2.pr
View file @ 41d0d5a6
......@@ -25,6 +25,12 @@
#define INVALID 255 /* set invalid data as garbage (i.e 255) */
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
typedef ObjRef {
byte objKey;
......
tests/case_studies/giop/giop3.nomig.pr
View file @ 41d0d5a6
......@@ -78,11 +78,8 @@ typedef MsgHeader {
byte request_id; /* Request, Reply, CancelRequest, */
/* LocateRequest, LocateReply */
byte object_key; /* Request, LocateRequest, */
/* bit response_expected; /* Request */
/* byte operation; /* Request */
byte reply_status; /* Reply */
byte forward_port; /* Reply -- LOCATION_FORWARD address */
/* byte locate_status; /* LocateReply */
byte tag;
}
......@@ -261,7 +258,7 @@ end: do
msg.mhdr.request_id = reqId;
msg.mhdr.object_key = objref.objKey;
msg.mhdr.tag = tag;
/* request_reqId = reqId; /* for validation */
/* request_reqId = reqId; for validation */
}
/* send the request */
lout!Request(svrPort, msg);
......@@ -292,7 +289,7 @@ CancelSent:
d_step {
reqId = msg.mhdr.request_id;
assert( usedReqId[reqId] != FREE );
/* reply_reqId = reqId; /* for validation */
/* reply_reqId = reqId; for validation */
}
ReplyRecvd:
......@@ -491,7 +488,7 @@ RequestRcvd:
d_step{
connState = AGENT_CONNECTED;
/* srequest_reqId = reqId; /* for validation */
/* srequest_reqId = reqId; for validation */
}
/* send server request */
......@@ -502,7 +499,7 @@ SRequestSent:
requested[reqId] = INUSE;
numOutstandingReqs = numOutstandingReqs + 1;
/* srequested[reqId] = TRUE; /* for validation */
/* srequested[reqId] = TRUE; for validation */
}
......@@ -531,7 +528,7 @@ SRequestSent:
/* send the Reply */
lout!Reply(clPort,msg);
ReplySent1:
/* numRepliesSent[port] = numRepliesSent[port] + 1; /* for validation */
/* numRepliesSent[port] = numRepliesSent[port] + 1; for validation */
skip;
fi;
......@@ -543,7 +540,7 @@ ReplySent1:
* that was not outstanding, this should never happen */
assert(requested[reqId] != FREE);
/* sreply_reqId = reqId; /* for validation */
/* sreply_reqId = reqId; for validation */
SReplyReceived:
if
......@@ -554,7 +551,7 @@ SReplyReceived:
requested[reqId] = FREE;
numOutstandingReqs = numOutstandingReqs - 1;
/* srequested[reqId] = FALSE; /* for validation */
/* srequested[reqId] = FALSE; for validation */
}
:: (requested[reqId] == INUSE) ->
......@@ -570,8 +567,8 @@ ReplySent2:
requested[reqId] = FREE;
numOutstandingReqs = numOutstandingReqs - 1;
/* srequested[reqId] = FALSE; /* for validation */
/* numRepliesSent[port] = numRepliesSent[port] + 1; /* for validation */
/* srequested[reqId] = FALSE; for validation */
/* numRepliesSent[port] = numRepliesSent[port] + 1; for validation */
}
fi;
......@@ -588,8 +585,8 @@ ReplySent2:
CloseConnectionSent:
d_step{
connState = AGENT_CLOSED;
/* numRequestsRcvd[port] = 0; /* for validation */
/* numRepliesSent[port] = 0; /* for validation */
/* numRequestsRcvd[port] = 0; for validation */
/* numRepliesSent[port] = 0; for validation */
}
:: (connState != AGENT_CONNECTED) ->
......@@ -723,7 +720,6 @@ resume:
/*--------------------------------------------------------------------------*/
init
{
/* create the processes from the bottom up */
atomic {
prid[0] = run transport(/*port*/ 0, toTransportU[0], toClientL );
......@@ -741,22 +737,10 @@ init
prid[8] = run Server(/*port*/ 1, /*objkey*/ 0 );
prid[9] = run Server(/*port*/ 2, /*objkey*/ 1 );
}
}
/* #include "never/v3.never" */
/* #include "never/v4_long.never" */
/* #include "never/v4a.never" */
/* #include "never/v4b.never" */
/* #include "never/v5.never" */
/* #include "never/v6a.never" */
/* #include "never/v6b.never" */
/* #include "never/v7.never" */
/* #include "never/v8.never" */
/* #include "never/v9a.never" */
/* #include "never/v9b.never" */
/* #include "never/v10.never" */
/*=========================================================================*/
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
tests/case_studies/giop/giop3.v10.nomig.pr
View file @ 41d0d5a6
......@@ -80,11 +80,8 @@ typedef MsgHeader {
byte request_id; /* Request, Reply, CancelRequest, */
/* LocateRequest, LocateReply */
byte object_key; /* Request, LocateRequest, */
/* bit response_expected; /* Request */
/* byte operation; /* Request */
byte reply_status; /* Reply */
byte forward_port; /* Reply -- LOCATION_FORWARD address */
/* byte locate_status; /* LocateReply */
byte tag;
}
......@@ -445,7 +442,7 @@ UserProcessed:
*User7Processed1: skip;
* :: else ->
* fi;
* /* end validation */
* end validation */
/* send the reply */
toAgentU[port]!SReply(objKey,opaqueData,opaqueData2)
......@@ -763,6 +760,13 @@ init
}
#include "never/v10.nomig.never"
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
/*#include "never/v10.nomig.never"
*/
/*=========================================================================*/
tests/case_studies/giop/giop3.v10.pr
View file @ 41d0d5a6
......@@ -80,11 +80,8 @@ typedef MsgHeader {
byte request_id; /* Request, Reply, CancelRequest, */
/* LocateRequest, LocateReply */
byte object_key; /* Request, LocateRequest, */
/* bit response_expected; /* Request */
/* byte operation; /* Request */
byte reply_status; /* Reply */
byte forward_port; /* Reply -- LOCATION_FORWARD address */
/* byte locate_status; /* LocateReply */
byte tag;
}
......@@ -797,7 +794,14 @@ init
}
}
#define __instances_User 2
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
/*
#include "never/v10.never"
*/
/*=========================================================================*/
tests/case_studies/giop/giop4.pr
View file @ 41d0d5a6
......@@ -14,6 +14,13 @@
/* Changed variable name pid to prid to avoid syntax error in SPIN V. 5
* Stefan Leue, 7.12.2008 */
#define __instances_User 5
#define __instances_GIOPClient 1
#define __instances_Server 2
#define __instances_GIOPAgent 2
#define __instances_transport 3
#define CHANLEN 5 /* default channel length (5) */
#define MAXREQID 5 /* maximum number for request_id (4) */
#define NUMOBJS 2 /* number of objects (2) */
......@@ -90,11 +97,8 @@ typedef MsgHeader {
byte request_id; /* Request, Reply, CancelRequest, */
/* LocateRequest, LocateReply */
byte object_key; /* Request, LocateRequest, */
/* bit response_expected; /* Request */
/* byte operation; /* Request */
byte reply_status; /* Reply */
byte forward_port; /* Reply -- LOCATION_FORWARD address */
/* byte locate_status; /* LocateReply */
}
......@@ -364,8 +368,7 @@ Reply0Recvd: skip
/* :: (cinfo[srcport].usedReqId[reqId] == CANCELLED) ->
* /* request was previously cancelled, so just free the request_id */
/* d_step{
d_step{
* cinfo[srcport].usedReqId[reqId] = FREE;
* cinfo[srcport].tags[reqId] = INVALID;
* }
......@@ -784,7 +787,7 @@ CloseConnectionSent:
}
/*:: lin?TAbortDisc-> /* need to cancel all outstanding requests */
/*:: lin?TAbortDisc-> need to cancel all outstanding requests */
od
}
......
tests/case_studies/giop/giop5.pr
View file @ 41d0d5a6
......@@ -89,11 +89,8 @@ typedef MsgHeader {
byte request_id; /* Request, Reply, CancelRequest, */
/* LocateRequest, LocateReply */
byte object_key; /* Request, LocateRequest, */
/* bit response_expected; /* Request */
/* byte operation; /* Request */
byte reply_status; /* Reply */
byte forward_port; /* Reply -- LOCATION_FORWARD address */
/* byte locate_status; /* LocateReply */
}
......@@ -179,7 +176,7 @@ proctype User(chan lin, lout)
objref.objKey = i;
objref.port = gPublished[i];
break;
:: (i < NUMOBJ - 1) ->
:: (i < NUMOBJS - 1) ->
i = i + 1;
od;
}
......@@ -364,8 +361,7 @@ Reply0Recvd: skip
/* :: (cinfo[srcport].usedReqId[reqId] == CANCELLED) ->
* /* request was previously cancelled, so just free the request_id */
/* d_step{
d_step{
* cinfo[srcport].usedReqId[reqId] = FREE;
* cinfo[srcport].tags[reqId] = INVALID;
* }
......@@ -784,7 +780,7 @@ CloseConnectionSent:
}
/*:: lin?TAbortDisc-> /* need to cancel all outstanding requests */
/*:: lin?TAbortDisc-> need to cancel all outstanding requests */
od
}
......@@ -940,6 +936,11 @@ init
}
#define __instances_User 5
#define __instances_GIOPClient 1
#define __instances_Server 10
#define __instances_GIOPAgent 2
#define __instances_transport 3
/* #include "never/v3.never" */
/* #include "never/v4.never" */
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment