Hi everyone!
I am trying to model a simple document processing system.
In my abstract spec I have defined a Process(document) operator. It simply changes a document state when called.
Now, in my refinement Spec I want to model batching (batches being created, cancelled, returning)
I want to keep the refinement relationship.
I have been trying to change the Process(document) operator to turn it into a higher order one:
Process(document) would become Process(processor(_),document), idea is that I would make processor(_) a constant that I could map in my refinement with:
AS = INSTANCE AbstractSpec WITH processor <- BatchProcessor
Except I have been hitting a wall:
in my cfg file I try to set processor(_) to use a basicProcessor operator but I get:
: Attempted to apply operator:
{ <_, basicProcessor>}
to arguments (d1), which is undefined.
Error: The behavior up to this point is:
State 1: <Initial predicate>
document_status = (d1 :> [queue |-> <<s_chunked, s_embedded, s_processed>>, state |-> s_new] @@ d2 :> [queue |-> <<s_chunked, s_embedded, s_processed>>, state |-> s_new] @@ d3 :> [queue |-> <<s_chunked, s_embedded, s_processed>>, state
|-> s_new] @@ d4 :> [queue |-> <<s_chunked, s_embedded, s_processed>>, state |-> s_new])
When I try to do the instanciation (in the supercession refinement which is an intermediate step between the abstract and batch spec) I also get this error:
line 18, col 1 to line 23, col 31 of module Supercession
Level error in instantiating module 'AuditCompanion':
The level of the _expression_ or operator substituted for 'processor'
must be at most 0.
I think I am missing something in the cfg file or trying to accomplish
something that might be unsupported. Being still a neophyte I'd be very
grateful for some help on this.