[tlaplus] Constant operator and refinements

[Quentin Mallet]

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.

[Stephan Merz]

You say that you intend the processor(_) operator to change the state of the document. But then it cannot be a constant operator, as it should be if it appears among the CONSTANT parameters. Indeed, basicProcessor(d) is an action formula, so SANY rightfully refuses to let you instantiate the parameter processor by basicProcessor.

If you want to have your specification be parameterized by document processors, you could introduce a (constant-level) operator parameter that takes both the current status and the document as arguments and returns the processed document as the result. Then you can write something like

document_status’ = [document_status EXCEPT ![d] = processor(document_status, d)]

in the definition of Next. In that case, the definition of basicProcessor would become

basicProcessor(ds, d) ==

   [state |-> Head(ds[d].queue), queue |-> Tail(ds[d].queue)]

Hope this helps,

Stephan

--
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 tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAMr%2BM%3DdygR_05PNv035qaqHCVVGFzPTQQv8fiYXhZhYPVMJ08w%40mail.gmail.com.
<AuditCompanion.cfg><AuditCompanion.tla><Supercession.tla><Supercession.cfg>

[Quentin Mallet]

Thank you very much, Stephan,

Indeed it looks like I was thinking too much like a programmer, your idea was the right one and my issue is solved!

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/E1C93948-D68C-479C-88CB-5F69C8FEE60B%40gmail.com.