This FDR release is for academic teaching and research purposes only.
For any other use, please contact Formal Systems (Europe) Ltd at
enquiries@fsel.com to obtain a commercial licence.
Checking scripts/DP5/ResourceAllocationVerificationEC0.csp
 Ready
/
Checking UserSpec(Phil.2) [F= Abs(Phil.2,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Asynchronous I/O unavailable with this build.
Using 1024 buffers of 128K
Refinement check: 
Refine checked 7 states
With 7 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking UserSpec(Phil.3) [F= Abs(Phil.3,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 7 states
With 7 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking UserSpec(Phil.4) [F= Abs(Phil.4,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 7 states
With 7 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking UserSpec(Phil.0) [F= Abs(Phil.0,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 7 states
With 7 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking UserSpec(Phil.1) [F= Abs(Phil.1,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 7 states
With 7 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking ResourceSpec(Fork.0) [F= Abs(Fork.0,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 3 states
With 4 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking ResourceSpec(Fork.3) [F= Abs(Fork.3,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 3 states
With 4 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking ResourceSpec(Fork.4) [F= Abs(Fork.4,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 3 states
With 4 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking ResourceSpec(Fork.1) [F= Abs(Fork.1,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 3 states
With 4 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true

Checking ResourceSpec(Fork.2) [F= Abs(Fork.2,EC0)
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
Starting timer
Starting compilation

Starting...
Compiling...
Reading...
Strong bisimulation: 
 Loading... done
Took 0(0+0) seconds
-- Normalising specification
-- Normalisation complete
Starting timer
About to start refinement
Refinement check: 
Refine checked 3 states
With 4 transitions
Allocated a total of 5 pages of size 128K
Compaction produced 0 chunks of 16K.
Took 0(0+0) seconds
true
