Changes between Version 10 and Version 11 of Introduction

Timestamp:

12/29/18 09:55:53 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -90 +90 @@
 The `$parfor` statement is a combination of `$for` and `$spawn`. The latter is very similar to a function call. The main difference is that the function called is invoked in a new process which runs concurrently with the existing processes.
 
-The program may be verified for an upper bound of 5 by typing the following at the command line:
+The program may be verified for an upper bound of 5 by typing
 
 {{{
@@ -96 +96 @@
 }}}
 
-which results in the following output (excerpted):
-
-{{{
+which results in the following output:
+
+{{{
+CIVL v1.18+ of 2018-12-28 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 21:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:20.32-32
+  $parfor(int i: 0..n-1) dine(i);
+                                ^
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:20.32 ";"
+process 1:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+process 2:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+
+Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
+Terminating search after finding 1 violation.
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl verify -inputB=5 diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.43
+   memory (bytes)      : 163053568
+   max process count   : 3
+   states              : 32
+   states saved        : 26
+   state matches       : 1
+   transitions         : 30
+   trace steps         : 21
+   valid calls         : 106
+   provers             : cvc4, z3
+   prover calls        : 4
 
 === Result ===
 The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
-
 }}}