On prover_id and component_id

Presently, a prover is identified by an attribute prover_id in display messages, which uniquely identifies the running instance of this prover. If we start a second instance, it will get another prover_id. This is bad, because it requires displays to keep the prover_id, but the main drawback is that we can't just restart a prover and let it re-use the source files the previous instance had already parsed and processed.

Therefore, I suggest that we identify the prover_id with the component_id of the prover. A component_id uniquely identifies one component, e.g. the prover "Isabelle 2005/HOL", but not its running instance. We can keep the name of the attribute.

This means that displays refer to a prover by "type", rather than a unique instance. The drawback is that we cannot support more than one running instance of the same prover, but given that this is bound to confuse the user anyway, this may be an advantage.

This change is wholly transparent to displays. We could make the startup/broker information protocol a bit simpler (but that would break compatibility with existing displays):

Present:

brokermsg  = 
    brokerstatus      # response to brokerstatusquery:
  | proveravailmsg      # announce new prover is available
  | newprovermsg      # new prover has started 
  | proverstatemsg      # prover state has changed (busy/ready/exit)

brokerstatus  = element brokerstatus 
                       { knownprovers, runningprovers, brokerinformation }

knownprover   = element knownprover   { componentid_attr, provername }
runningprover = element runningprover { componentid_attr, proverid_attr, provername }

knownprovers   = element knownprovers { knownprover* }
runningprovers = element runningprovers { runningprover* }
brokerinformation = element brokerinformation { text }

proveravailmsg  = element proveravailable { provername_attr,
                                            componentid_attr }
newprovermsg    = element proverstarted { proverid_attr
               , componentid_attr
                              , provername_attr
                              }
proverstatemsg = element proverstate { 
                       proverid_attr, provername_attr,
                       attribute proverstate {proverstate} } 

proverstate    = ("ready" | "busy" | "exitus")

Suggested changes:

  • remove knownbrokers, runningprovers message, and replace brokerstatus with the following, so the broker just reports the state of all provers it knows (the state will show wether provers are running or not):
brokerstatus  = element brokerstatus {proverstatemsg*, brokerinformation }
  • remove newprovermsg (and replace it with appropriate proverstatemsg).
  • Rename componentid_attr in proveravailmsg to proverid_attr to be consistent.
  • Do we need a new proverstate "started" for provers having just started?

Suggestion is to first implement the new meaning of prover_id as suggested above, and keep the old brokercontrol messages for a while.

-- ChristophLueth - 26 Sep 2006

Edit | Attach | Print version | History: r4 < r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r3 - 28 Sep 2006 - 22:38:43 - ChristophLueth
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies