Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
M MTSA
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 68
    • Issues 68
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Metrics
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Package Registry
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • lafhis
  • MTSA
  • Issues
  • #74

Closed
Open
Created May 26, 2025 by Sebastian Uchitel@suchitelOwner

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 } }.

Edited May 26, 2025 by Sebastian Uchitel
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking