Irrelevant warning when relabeling LTS
When compiling LTS sometimes the prints in the output pane the text: Warning - Relabeling with maybe actions can only be made over labels and sets.
This should only occur when what is being compiled is an MTS. This is not the case.
For the folling input, if you compile VERIFY_MUSEO2 you get the warning. On the other hand if you delete everything from line 38 ("//es.4") the warning is not produced.
Input: // es.3 - MUSEO const N = 10 ENTRADA = (ticket -> entry -> ENTRADA).
SALIDA = (exit->SALIDA).
DIRECTOR = (open -> close -> empty -> DIRECTOR).
CONTROL = (open -> ABIERTO[0]), ABIERTO[i:0..N] = (when(i<N) ticket->entry->ABIERTO[i+1] | when(i>0) exit -> ABIERTO[i-1] | close -> CERRADO[i]), CERRADO[i:0..N] = (when(i>0) exit -> CERRADO[i-1] | when(i==0) empty -> CONTROL).
||MUSEO = (ENTRADA || SALIDA || DIRECTOR || CONTROL).
//property -> no se puede ingresar al museo si esta cerrado property MUSEO_OBS1 = (close -> MUSEO_OBS1 | open -> OBS_ABIERTO), //SOLO ACEPTA CLOSE OR OPEN, NO ACEPTA TICKET, ASSUMPTION EMPIEZA CERRADO OBS_ABIERTO = ({open,ticket}->OBS_ABIERTO | close -> MUSEO_OBS1).
||VERIFY_MUSEO1 = (MUSEO || MUSEO_OBS1).
//property -> no se puede salir del museo si esta cerrado
property MUSEO_OBS2 = (close -> MUSEO_OBS1 | open -> OBS_ABIERTO),
OBS_ABIERTO = ({open,exit}->OBS_ABIERTO | close -> MUSEO_OBS2).
||VERIFY_MUSEO2 = (MUSEO || MUSEO_OBS2).
//EL CONTRAEJEMPLO DE LA HERRAMIENTA // OPEN - TICKET - ENTRY - CLOSE - EXIT
//es.4 //leader election in a synchronous ring set UID = {[19],[14],[7],[2]} const K = #UID set M = {null,msg.UID} set Status = {unknown, leader} //links or channels hold at most a single message CHAN = (put[m:M]-> get[m]-> CHAN). //the synchronous model proceeds in two steps ROUND = (step1-> step2-> ROUND). //the processes PROCESS(U=1) = (init[U]->STATE['unknown]['msg[U]]), STATE[status:Status][send:M] = (step1-> put[send]-> STATE[status][send] |step2-> (get.null-> DSTATE[status]['null] |get.msg[v:UID]-> if (v>U) then DSTATE[status]['msg[v]] else if (v==U) then DSTATE['leader]['null] else DSTATE[status]['null] ) ), DSTATE[status:Status][send:M] = ([send]->[status]->STATE[status][send]). ||LCR = ( ROUND || chan[1..K]:CHAN || proc[i:1..K]:PROCESS(@(UID,i-1)) )/{ forall[i:1..K] { proc[i].get/chan[i].get, proc[i].put/chan[i%K+1].put, step1/proc[i].step1, step2/proc[i].step2 } }.