Sistema de Transiciones: Elevador

A continuación veremos mi sistema de transiciones que consiste en un elevador y una puerta, basandome en la entrada anterior en donde modele el mismo sistema hice el sistema de transiciones en donde también se corrigieron unos errores cometidos en el modelo de la red petri en donde nunca regresaba a un estado inicial.

Y este es el código que hice en promela basandome en la explicación de las diapositivas que dejaré debajo.

	int puerta;
	int actual;
	bool moviendo;
	proctype Inicio(){
	atomic {
	(actual != null) -> moviendo = true
	}
	}
	proctype Baja(int puerta, bool moviendo){
	atomic {
	(puerta < actual) -> puerta = puerta - 1, moviendo = true
	}
	}
	proctype Detiene(int puerta, bool moviendo){
	atomic {
	(puerta == actual) -> moviendo = false
	}
	}
	proctype Sube(int puerta, bool moviendo){
	atomic {
	(puerta > actual) -> puerta = puerta + 1, moviendo = true
	}
	}
	proctype secuencia() {
	do
	:: (puerta != 0) ->
	if
	:: (puerta < actual) -> Baja(puerta, moviendo)
	:: (puerta > actual) -> Sube(puerta, moviendo)
	:: (puerta == actual) -> Detiene(puerta, moviendo)
	fi
	od
	}
	init {
	do
	:: (True) ->
	run Inicio()
	run secuencia()
	od
	}

view raw gistfile1.c hosted with ❤ by GitHub

Fuente:
Diapositivas de promela.