- New claim: CLAIM_Reachable

- Added new switches:
  -G,--generate-statespace
  -C,--generate-claims
- Claims are now allowed to have no label (they will be generated
  automatically)
- Output summary shows parameter of claims
- Internally, new symbols can now be generated by
  symbolNextFree(prefixsymbol)

src/compiler.c

@@ -355,15 +355,130 @@ levelTacDeclaration (Tac tc, int isVar)
       /* declare this variable/constant with the previously derived type list */
       t = symbolDeclare (tscan->t1.sym, isVar);
       t->stype = typetl;
-      if (isVar && level == 2)
+      /* local to the role? */
+      if (level == 2)
 	{
-	  /* it is a role variable, so add it to the nicely declared variables */
+	  if (isVar)
-	  thisRole->declaredvars = termlistAdd (thisRole->declaredvars, t);
+	    {
+	      /* it is a role variable, so add it to the nicely declared variables */
+	      thisRole->declaredvars =
+		termlistAdd (thisRole->declaredvars, t);
+	    }
+	  else
+	    {
+	      /* it is a role constant, so add it to the nicely declared constants */
+	      thisRole->declaredconsts =
+		termlistAdd (thisRole->declaredconsts, t);
+	    }
 	}
       tscan = tscan->next;
     }
 }
 
+//! Check whether a claim label already occurs
+int
+isClaimlabelUsed (const System sys, const Term label)
+{
+  Claimlist cl;
+
+  if (label == NULL)
+    {
+      /* we assign this 'occurs' because it is an invalid label */
+      return true;
+    }
+  cl = sys->claimlist;
+  while (cl != NULL)
+    {
+      if (isTermEqual (cl->label, label))
+	{
+	  return true;
+	}
+      cl = cl->next;
+    }
+  return false;
+}
+
+//! Generate a fresh claim label
+Term
+generateFreshClaimlabel (const System sys, const Role role, const Term claim)
+{
+  /* Simply use the role as a prefix */
+  return freshTermPrefix (role->nameterm);
+}
+
+//! Create a claim and add it to the claims list, and add the role event.
+Claimlist
+claimCreate (const System sys, const Protocol protocol, const Role role,
+	     const Term claim, Term label, const Term msg)
+{
+  Claimlist cl;
+  Term labeltuple;
+
+  /* check for ignored claim types */
+  if (switches.filterClaim != NULL && switches.filterClaim != claim)
+    {
+      /* abort the construction of the node */
+      return;
+    }
+
+  /* generate full unique label */
+  /* is the label empty or used? */
+  if (label == NULL || isClaimlabelUsed (sys, label))
+    {
+      /* simply generate a fresh one */
+      label = generateFreshClaimlabel (sys, role, claim);
+    }
+
+  // Assert: label is unique, add claimlist info
+  cl = memAlloc (sizeof (struct claimlist));
+  cl->type = claim;
+  cl->label = label;
+  cl->parameter = msg;
+  cl->protocol = thisProtocol;
+  cl->rolename = role->nameterm;
+  cl->role = role;
+  cl->roledef = NULL;
+  cl->count = 0;
+  cl->complete = 0;
+  cl->timebound = 0;
+  cl->failed = 0;
+  cl->prec = NULL;
+  cl->roles = NULL;
+  cl->alwaystrue = false;
+  cl->warnings = false;
+  cl->next = sys->claimlist;
+  sys->claimlist = cl;
+
+  /* add the role event */
+  role->roledef = roledefAdd (role->roledef, CLAIM, label,
+			      role->nameterm, claim, msg, cl);
+
+  /* possible special handlers for each claim */
+
+  if (claim == CLAIM_Secret)
+    {
+      Termlist claimvars;
+      Termlist readvars;
+
+      /* now check whether the claim contains variables that can actually be influenced by the intruder */
+
+      claimvars = termlistAddVariables (NULL, msg);
+      readvars = compute_read_variables (thisRole);
+      while (claimvars != NULL)
+	{
+	  if (!inTermlist (readvars, claimvars->term))
+	    {
+	      /* this claimvar does not occur in the reads? */
+	      /* then we should ignore it later */
+	      cl->alwaystrue = true;
+	      cl->warnings = true;
+	    }
+	  claimvars = claimvars->next;
+	}
+    }
+}
+
+//! Parse a communication event tc of type event, and add a role definition event for it.
 void
 commEvent (int event, Tac tc)
 {
@@ -382,7 +497,12 @@ commEvent (int event, Tac tc)
   /* Construct label, if any */
   if (tc->t1.sym == NULL)
     {
-      label = NULL;
+      /* right, now this should not be NULL anyway, if so we construct a fresh one.
+       * This can be a weird choice if it is a read or send, because in that case
+       * we cannot chain them anymore and the send-read correspondence is lost.
+       */
+      warning ("Generated fresh label for line %i.", tc->lineno);
+      label = freshTermPrefix (thisRole->nameterm);
     }
   else
     {
@@ -398,21 +518,10 @@ commEvent (int event, Tac tc)
 	}
       else
 	{
-	  /* we already had this label constant */
 	  /* leaves a garbage tuple. dunnoh what to do with it */
 	  label = makeTermTuple (thisProtocol->nameterm, label);
 	}
     }
-  /**
-   * We now know the label. Find the corresponding labelinfo bit or make a new one
-   */
-  linfo = label_find (sys->labellist, label);
-  if (linfo == NULL)
-    {
-      /* Not found, make a new one */
-      linfo = label_create (label, thisProtocol);
-      sys->labellist = list_append (sys->labellist, linfo);
-    }
 
   /**
    * Parse the specific event type
@@ -422,6 +531,17 @@ commEvent (int event, Tac tc)
     {
     case READ:
     case SEND:
+      /**
+       * We know the label. Find the corresponding labelinfo bit or make a new one
+       */
+      linfo = label_find (sys->labellist, label);
+      if (linfo == NULL)
+	{
+	  /* Not found, make a new one */
+	  linfo = label_create (label, thisProtocol);
+	  sys->labellist = list_append (sys->labellist, linfo);
+	}
+
       /* now parse triplet info */
       if (trip == NULL || trip->next == NULL || trip->next->next == NULL)
 	{
@@ -461,8 +581,13 @@ commEvent (int event, Tac tc)
 	  linfo->readrole = torole;
 	}
 
+      /* and make that read/send event */
+      thisRole->roledef = roledefAdd (thisRole->roledef, event, label,
+				      fromrole, torole, msg, cl);
       break;
+
     case CLAIM:
+      /* switch can be used to remove all *parsed* claims */
       if (!switches.removeclaims)
 	{
 	  /* now parse tuple info */
@@ -477,13 +602,6 @@ commEvent (int event, Tac tc)
 	  claim = tupleProject (claimbig, 0);
 	  torole = claim;
 
-	  /* check for ignored claim types */
-	  if (switches.filterClaim != NULL && switches.filterClaim != claim)
-	    {
-	      /* abort the construction of the node */
-	      return;
-	    }
-
 	  /* check for obvious flaws */
 	  if (claim == NULL)
 	    {
@@ -491,7 +609,7 @@ commEvent (int event, Tac tc)
 	    }
 	  if (!inTermlist (claim->stype, TERM_Claim))
 	    {
-	      printf ("error: unknown claim type ");
+	      printf ("error: claim term is not of claim type ");
 	      termPrint (claim);
 	      errorTac (trip->next->lineno);
 	    }
@@ -514,50 +632,21 @@ commEvent (int event, Tac tc)
 		}
 	    }
 
-	  /* store claim in claim list */
+	  // check whether label is unique
 
-	  if (label == NULL)
+	  if (isClaimlabelUsed (sys, label))
 	    {
-	      error ("Claim should have label on line %i.",
+	      warning
-		     trip->next->lineno);
+		("Claim label is not unique at line %i, generating fresh label.",
+		 tc->lineno);
 	    }
-	  // First check whether label is unique
+
-	  cl = sys->claimlist;
-	  while (cl != NULL)
-	    {
-	      if (isTermEqual (cl->label, label))
-		{
-		  /**
-		   *@todo This should not error exit, but automatically generate a fresh claim label.
-		   */
-		  error ("Claim label is not unique at line %i.", tc->lineno);
-		}
-	      cl = cl->next;
-	    }
-	  // Assert: label is unique, add claimlist info
-	  cl = memAlloc (sizeof (struct claimlist));
-	  cl->type = claim;
-	  cl->label = label;
-	  cl->protocol = thisProtocol;
-	  cl->rolename = fromrole;
-	  cl->role = thisRole;
 	  if (!isTermEqual (fromrole, thisRole->nameterm))
 	    error
 	      ("Claim role does not correspond to execution role at line %i.",
 	       tc->lineno);
-	  cl->roledef = NULL;
-	  cl->count = 0;
-	  cl->complete = 0;
-	  cl->timebound = 0;
-	  cl->failed = 0;
-	  cl->prec = NULL;
-	  cl->roles = NULL;
-	  cl->alwaystrue = false;
-	  cl->warnings = false;
-	  cl->next = sys->claimlist;
-	  sys->claimlist = cl;
 
-	  /* handles all claim types differently */
+	  /* handles claim types with different syntactic claims */
 
 	  if (claim == CLAIM_Secret)
 	    {
@@ -573,26 +662,6 @@ commEvent (int event, Tac tc)
 		    ("Secrecy claim on line %i should not contain tuples (for Arachne) until it is officially supported.",
 		     trip->next->lineno);
 		}
-	      /* now check whether the claim contains variables that can actually be influenced by the intruder */
-	      {
-		Termlist claimvars;
-		Termlist readvars;
-
-		claimvars = termlistAddVariables (NULL, msg);
-		readvars = compute_read_variables (thisRole);
-		while (claimvars != NULL)
-		  {
-		    if (!inTermlist (readvars, claimvars->term))
-		      {
-			/* this claimvar does not occur in the reads? */
-			/* then we should ignore it later */
-			cl->alwaystrue = true;
-			cl->warnings = true;
-		      }
-		    claimvars = claimvars->next;
-		  }
-	      }
-	      break;
 	    }
 	  if (claim == CLAIM_Nisynch)
 	    {
@@ -601,7 +670,6 @@ commEvent (int event, Tac tc)
 		  error ("NISYNCH claim requires no parameters at line %i.",
 			 trip->next->lineno);
 		}
-	      break;
 	    }
 	  if (claim == CLAIM_Niagree)
 	    {
@@ -610,25 +678,14 @@ commEvent (int event, Tac tc)
 		  error ("NIAGREE claim requires no parameters at line %i.",
 			 trip->next->lineno);
 		}
-	      break;
-	    }
-	  if (claim == CLAIM_Empty)
-	    {
-	      break;
 	    }
 
-	  /* hmm, no handler yet */
+	  /* create the event */
 
-	  printf ("error: No know handler for this claim type: ");
+	  cl = claimCreate (sys, thisProtocol, thisRole, claim, label, msg);
-	  termPrint (claim);
-	  printf (" ");
-	  errorTac (trip->next->lineno);
 	}
       break;
     }
-  /* and make that event */
-  thisRole->roledef = roledefAdd (thisRole->roledef, event, label,
-				  fromrole, torole, msg, cl);
 }
 
 int
@@ -663,6 +720,28 @@ normalDeclaration (Tac tc)
   return 1;
 }
 
+//! Add all sorts of claims to this role
+void
+claimAddAll (const System sys, const Protocol protocol, const Role role)
+{
+  /* first: secrecy claims for all locally declared things */
+  void addSecrecyList (Termlist tl)
+  {
+    while (tl != NULL)
+      {
+	claimCreate (sys, protocol, role, CLAIM_Secret, NULL, tl->term);
+	tl = tl->next;
+      }
+  }
+
+  addSecrecyList (role->declaredconsts);
+  addSecrecyList (role->declaredvars);
+
+  /* full non-injective agreement and ni-synch */
+  claimCreate (sys, protocol, role, CLAIM_Niagree, NULL, NULL);
+  claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL);
+}
+
 void
 roleCompile (Term nameterm, Tac tc)
 {
@@ -726,6 +805,19 @@ roleCompile (Term nameterm, Tac tc)
 	tc = tc->next;
       }
   }
+
+  /* add any claims according to the switches */
+
+  if (switches.addreachableclaim)
+    {
+      claimCreate (sys, thisProtocol, thisRole, CLAIM_Reachable, NULL, NULL);
+    }
+  if (switches.addallclaims)
+    {
+      claimAddAll (sys, thisProtocol, thisRole);
+    }
+
+  /* last bits */
   compute_role_variables (sys, thisProtocol, thisRole);
   levelDone ();
 }

src/main.c

@@ -370,47 +370,104 @@ timersPrint (const System sys)
   /* Note that if the output is set to empty, the claim output is redirected to stdout (for e.g. processing)
    */
   cl_scan = sys->claimlist;
-  anyclaims = 0;
+  anyclaims = false;
   while (cl_scan != NULL)
     {
       if (!isTermEqual (cl_scan->type, CLAIM_Empty))
 	{
-	  anyclaims = 1;
+	  Protocol protocol;
+	  Term pname;
+	  Term rname;
+	  Termlist labellist;
+
+	  anyclaims = true;
 
 	  eprintf ("claim\t");
 
-	  /* claim label is tuple */
+	  protocol = (Protocol) cl_scan->protocol;
-	  if (realTermTuple (cl_scan->label))
+	  pname = protocol->nameterm;
+	  rname = cl_scan->rolename;
+
+	  labellist = tuple_to_termlist (cl_scan->label);
+
+	  /* maybe the label contains duplicate info: if so, we remove it here */
+	  {
+	    Termlist tl;
+	    tl = labellist;
+	    while (tl != NULL)
+	      {
+		if (isTermEqual (tl->term, pname)
+		    || isTermEqual (tl->term, rname))
+		  {
+		    tl = termlistDelTerm (tl);
+		    labellist = tl;
+		  }
+		else
+		  {
+		    tl = tl->next;
+		  }
+	      }
+	  }
+
+	  termPrint (pname);
+	  eprintf (",");
+	  termPrint (rname);
+	  eprintf ("\t");
+	  /* second print event_label */
+	  termPrint (cl_scan->type);
+
+	  eprintf ("_");
+	  if (labellist != NULL)
 	    {
-	      /* modern version: claim label is tuple (protocname, label) */
+	      Termlist tl;
-	      /* first print protocol.role */
+
-	      termPrint (TermOp1 (cl_scan->label));
+	      tl = labellist;
-	      eprintf (",");
+	      while (tl != NULL)
-	      termPrint (cl_scan->rolename);
+		{
-	      eprintf ("\t");
+		  termPrint (tl->term);
-	      /* second print event_label */
+		  tl = tl->next;
-	      termPrint (cl_scan->type);
+		  if (tl != NULL)
-	      eprintf ("_");
+		    {
-	      termPrint (TermOp2 (cl_scan->label));
+		      eprintf (",");
-	      eprintf ("\t");
+		    }
+		}
+	      /* clean up */
+	      termlistDelete (labellist);
+	      labellist = NULL;
 	    }
 	  else
 	    {
-	      /* old-fashioned output */
+	      eprintf ("?");
-	      termPrint (cl_scan->type);
+	    }
-	      eprintf ("\t");
+	  /* add parameter */
-	      termPrint (cl_scan->rolename);
+	  eprintf ("\t");
-	      eprintf (" (");
+	  if (cl_scan->parameter != NULL)
-	      termPrint (cl_scan->label);
+	    {
-	      eprintf (")\t");
+	      termPrint (cl_scan->parameter);
+	    }
+	  else
+	    {
+	      eprintf ("-");
 	    }
 
 	  /* now report the status */
+	  eprintf ("\t");
 	  eprintf ("attacks: ");
 	  if (cl_scan->count > 0 && cl_scan->failed > 0)
 	    {
 	      /* there is an attack */
-	      eprintf ("yes\t(at least %i)", cl_scan->failed);
+	      eprintf ("yes\t");
+	      /* are these all attacks? */
+	      eprintf ("(");
+	      if (cl_scan->complete)
+		{
+		  eprintf ("exactly");
+		}
+	      else
+		{
+		  eprintf ("at least");
+		}
+	      eprintf (" %i)", cl_scan->failed);
 	    }
 	  else
 	    {

src/parser.y

@@ -48,6 +48,7 @@ int yylex(void);
 %type	<tac>	roleref
 
 %type	<symb>	label
+%type	<symb>	optlabel
 
 %start spdlcomplete
 
@@ -142,7 +143,7 @@ event		: READT label '(' termlist ')' ';'
 			t->t2.tac = $4;
 			$$ = t;
 		  }
-		| CLAIMT label '(' termlist ')' ';'
+		| CLAIMT optlabel '(' termlist ')' ';'
 		/* TODO maybe claims should be in the syntax */
 		  {	Tac t = tacCreate(TAC_CLAIM);
 		  	t->t1.sym = $2;
@@ -226,11 +227,17 @@ typeinfoN	: /* empty */
 		  }
 		;
 
-/* Previously, the label could be omitted. It is now required. */
 label		: '_' ID
 		  { $$ = $2; }
 		;
 
+optlabel        : /* empty */
+                 { $$ = NULL; }
+               | label
+		  { }
+                ;
+
+
 term  		: ID
 		  {
 		  	Tac t = tacCreate(TAC_STRING);

src/role.c

@@ -241,6 +241,7 @@ roleCreate (Term name)
   r->locals = NULL;
   r->variables = NULL;
   r->declaredvars = NULL;
+  r->declaredconsts = NULL;
   r->initiator = 1;		//! Will be determined later, if a read is the first action (in compiler.c)
   r->next = NULL;
   return r;

src/role.h

@@ -18,6 +18,8 @@ struct claimlist
   Term type;
   //! The term element for this node.
   Term label;
+  //! Any parameters
+  Term parameter;
   //! The pointer to the protocol (not defined typically, because
   //! at compile time of the claim the protocol structure is not known yet.)
   void *protocol;
@@ -124,6 +126,8 @@ struct role
   Termlist locals;
   //! Local variables for this role.
   Termlist variables;
+  //! Declared constants for this role
+  Termlist declaredconsts;
   //! Declared variables for this role
   Termlist declaredvars;
   //! Flag for initiator roles

src/specialterm.c

@@ -26,6 +26,7 @@ Term CLAIM_Secret;
 Term CLAIM_Nisynch;
 Term CLAIM_Niagree;
 Term CLAIM_Empty;
+Term CLAIM_Reachable;
 
 //! Init special terms
 /**
@@ -50,4 +51,5 @@ specialTermInit (const System sys)
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
   langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
   langcons (CLAIM_Empty, "Empty", TERM_Claim);
+  langcons (CLAIM_Reachable, "Reachable", TERM_Claim);
 }

src/specialterm.h

@@ -18,5 +18,6 @@ extern Term CLAIM_Secret;
 extern Term CLAIM_Nisynch;
 extern Term CLAIM_Niagree;
 extern Term CLAIM_Empty;
+extern Term CLAIM_Reachable;
 
 #endif

src/switches.c

@@ -75,6 +75,8 @@ switchesInit (int argc, char **argv)
   switches.switchP = 0;		// multi-purpose parameter
   switches.experimental = 0;	// experimental stuff defaults to 0, whatever that means.
   switches.removeclaims = false;	// default: leave claims from spdl file
+  switches.addreachableclaim = false;	// add 'reachable' claims
+  switches.addallclaims = false;	// add all sorts of claims
 
   // Output
   switches.output = SUMMARY;	// default is to show a summary
@@ -395,6 +397,37 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect ('C', "generate-claims", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-C,--generate-claims",
+		    "ignore any existing claims and automatically generate new claims");
+	}
+      else
+	{
+	  switches.removeclaims = true;
+	  switches.addallclaims = true;
+	  return index;
+	}
+    }
+
+  if (detect ('G', "generate-semibundles", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-G,--generate-statespace",
+		    "ignore any existing claims and add 'reachable' claims to generate the full state space");
+	}
+      else
+	{
+	  switches.removeclaims = true;	// remove parsed claims
+	  switches.addreachableclaim = true;	// add reachability claims
+	  switches.prune = 0;	// do not prune anything
+	  return index;
+	}
+    }
+
   /* ==================
    *  Bounding options
    */

src/switches.h

@@ -54,6 +54,8 @@ struct switchdata
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
   int experimental;		//!< Experimental stuff goes here until it moves into main stuff.
   int removeclaims;		//!< Remove any claims in the spdl file
+  int addreachableclaim;	//!< Adds 'reachable' claims to each role
+  int addallclaims;		//!< Adds all sorts of claims to the roles
 
   // Output
   int output;			//!< From enum outputs: what should be produced. Default ATTACK.

src/symbol.c

@@ -211,6 +211,60 @@ symbolSysConst (const char *str)
   return symb;
 }
 
+//! Generate the first fresh free number symbol, prefixed by a certain symbol's string.
+/**
+ * Note that there is an upper limit to this, to avoid some problems with buffer overflows etc.
+ */
+Symbol
+symbolNextFree (Symbol prefixsymbol)
+{
+  char *prefixstr;
+  int n;
+  int len;
+
+  if (prefixsymbol != NULL)
+    {
+      prefixstr = (char *) prefixsymbol->text;
+    }
+  else
+    {
+      prefixstr = "";
+    }
+
+  len = strlen (prefixstr);
+  n = 1;
+  while (n <= 9999)
+    {
+      char buffer[len + 5];	// thus we must enforce a maximum of 9.999 (allowing for storage of \0 )
+      Symbol symb;
+      int slen;
+
+      slen = sprintf (buffer, "%s%i", prefixstr, n);
+      symb = lookup (buffer);
+      if (symb == NULL)
+	{
+	  char *newstring;
+	  // Copy the buffer to something that will survive
+	  /**
+	   * Memory leak: although this routine should not be called recursively, it will never de-allocate this memory.
+	   * Thus, some precaution is necessary.
+	   * [x][CC]
+	   */
+	  newstring = (char *) memAlloc (slen + 1);
+	  memcpy (newstring, buffer, slen + 1);
+
+	  /* This persistent string can be used to return a fresh symbol */
+
+	  return symbolSysConst (newstring);
+	}
+
+      // Try next one
+      n++;
+    }
+  error ("We ran out of numbers (%i) when trying to generate a fresh symbol.",
+	 n);
+}
+
 //! Fix all the unset keylevels
 void
 symbol_fix_keylevels (void)

src/symbol.h

@@ -44,6 +44,7 @@ void symbolPrint (const Symbol s);
 void symbolPrintAll (void);
 Symbol symbolSysConst (const char *str);
 void symbol_fix_keylevels (void);
+Symbol symbolNextFree (Symbol prefixsymbol);
 
 void eprintf (char *fmt, ...);
 

src/term.c

@@ -1336,3 +1336,19 @@ isLeafNameEqual (Term t1, Term t2)
 {
   return (TermSymb (t1) == TermSymb (t2));
 }
+
+//! Generate a fresh term, that does not occur yet, prefixed with the string of the given term.
+Term
+freshTermPrefix (Term prefixterm)
+{
+  Symbol prefixsymbol;
+  Symbol freshsymbol;
+
+  prefixsymbol = NULL;
+  if (prefixterm != NULL && realTermLeaf (prefixterm))
+    {
+      prefixsymbol = TermSymb (prefixterm);
+    }
+  freshsymbol = symbolNextFree (prefixsymbol);
+  return makeTermType (GLOBAL, freshsymbol, -1);
+}

src/term.h

@@ -196,5 +196,6 @@ float term_constrain_level (const Term term);
 void term_set_keylevels (const Term term);
 void termPrintDiff (Term t1, Term t2);
 int isLeafNameEqual (Term t1, Term t2);
+Term freshTermPrefix (Term prefixterm);
 
 #endif