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.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.