1.

SMS

tipo SMS { observador nroDestino (s: SMS) : Numero ; observador texto (s: SMS) : Texto ; invariante noEstaVacio : |texto(s)| > 0 ; invariante noSupera160 : |texto(s)| ≤ 160 ; } problema nuevoSMS (n: Numero, t: Texto) = result : SMS { requiere 0 < |t| ≤ 160 ; asegura nroDestino(result) == n ∧ texto(result) == t ; } problema nroDestinoSMS (s: SMS) = result : Numero { asegura result == nroDestino(s) ; } problema textoSMS (s: SMS) = result : Texto { asegura result == texto(s) ; }

1

2.

Pregunta

tipo Pregunta { observador texto (p: Pregunta) : Texto ; observador rtaCorrecta (p: Pregunta) : Texto ; observador puntaje (p: Pregunta) : Puntaje ; invariante puntajesPositivos : puntaje(p) > 0 ; } problema nuevaP (t, r: Texto, p: Puntaje) = result : Pregunta { requiere p > 0 ; asegura texto(result) == t ∧ rtaCorrecta(result) == r ∧ puntaje(result) == p ; } problema textoP (p: Pregunta) = result : Texto { asegura result == texto(p) ; } problema rtaCorrectaP (p: Pregunta) = result : Texto { asegura result == rtaCorrecta(p) ; } problema puntajeP (p: Pregunta) = result : Puntaje { asegura result == puntaje(p) ; }

2

3.

Trivia

tipo Trivia { observador keywords (t: Trivia) : [Keyword] ; observador preguntas (t: Trivia) : [Pregunta] ; observador participantes (t: Trivia) : [Usuario] ; observador ganadores (t: Trivia) : [Usuario] ; observador proxPregunta (t: Trivia, u: Usuario) : Pregunta ; requiere u ∈ participantes(t) ∧ u ∈ / ganadores(t) ; observador puntajeAcumulado (t: Trivia, u: Usuario) : Puntaje ; requiere u ∈ participantes(t) ; invariante noEsTrivialGanar : |preguntas(t)| > 0 ; invariante noHayPreguntasRepetidas : (∀i, j ← [0..|preguntas(t)|), i 6= j) texto(preguntas(t)i ) 6= texto(preguntas(t)j ) ; invariante noHayUsuariosRepetidos : sinRepetidos(participantes(t)) ∧ sinRepetidos(ganadores(t)) ; invariante proxPreguntaValida : (∀u ← participantes(t), p ∈ / ganadores(t))proxP regunta(t, u) ∈ preguntas(t) ; invariante puntajesNoNegativos : (∀u ← participantes(t))puntajeAcumulado(t, u) ≥ 0 ; invariante preguntasEntranEnSMS : (∀p ← preguntas(t))0 < |texto(p)| ≤ 139 ; P invariante maximoPuntaje : [puntaje(p)|p ← preguntas(t)] ≤ 999 ; invariante losGanadoresSonParticipantes : (∀g ← ganadores(t))g ∈ participantes(t) ; } problema nuevaT (ks: [Keyword], ps: [Pregunta]) = result : Trivia { requiere |ps| > 0 ; requiere (∀i, j ← [0..|ps|), i 6= j)texto(psi ) 6= texto(psj ) ; requiere (∀p P ← ps)0 < |texto(p)| ≤ 139 ; requiere [puntaje(p)|p ← ps] ≤ 999 ; asegura mismos(keywords(result), ks) ; asegura preguntas(result) == ps ; asegura |(participantes(result))| == 0 ; asegura |(ganadores(result))| == 0 ; } problema preguntasT (t: Trivia) = result : [Pregunta] { asegura result == preguntas(t) ; } problema keywordsT (t: Trivia) = result : [Keyword] { asegura result == keywords(t) ; } problema participantesT (t: Trivia) = result : [Usuario] { asegura mismos(result, participantes(t)) ; } problema ganadoresT (t: Trivia) = result : [Usuario] { asegura result == ganadores(t) ; } problema proxPreguntaParticipanteT (t: Trivia, u: Usuario) = result : Pregunta { requiere u ∈ participantes(t) ∧ u ∈ / ganadores(t) ; asegura result == proxP regunta(t, u) ; } problema puntajeAcumuladoT (t: Trivia, u: Usuario) = result : Puntaje { requiere u ∈ participantes(t) ; asegura result == puntajeAcumulado(t, u) ; } problema registrarJugadorT (t: Trivia, u: Usuario, k: Keyword) = result : (Trivia,SMS) { requiere keywordValida : k ∈ keywords(t) ; requiere noEstaRegistrado : u ∈ / participantes(t) ; asegura seMantienenKeywords : mismos(keywords(prm(result)), keywords(t)) ; asegura seMantienenPreguntas : preguntas(prm(result)) == preguntas(t) ; asegura seAgregaParticipante : mismos(participantes(prm(result)), u : participantes(t)) ; 3

asegura seMantienenGanadores : ganadores(prm(result)) == ganadores(t) ; asegura otrosParticipantesMantienenEstado : (∀p ← participantes(t))puntajeAcumulado(prm(result), p) == puntajeAcumulado(t, p) ∧ (p ∈ / ganadores(t) → proxP regunta(prm(result), p) == proxP regunta(t, p)) ; asegura empiezaPorElPrincipio : proxP regunta(prm(result), u) == preguntas(prm(result))0 ; asegura empiezaSinPuntos : puntajeAcumulado(prm(result), u) == 0 ; asegura smsBienvenidaOK : esM ensajeP rimerP regunta(sgd(result), prm(result), u) ; } problema desregistrarJugadorT (t: Trivia, u: Usuario) = result : Trivia { requiere estaRegistrado : u ∈ participantes(t) ; asegura seMantienenKeywords : mismos(keywords(result), keywords(t)) ; asegura seMantienenPreguntas : preguntas(result) == preguntas(t) ; asegura seEliminaParticipante : mismos(u : participantes(result), participantes(t)) ; asegura quedanGanadores : ganadores(result) == [ g | g ← ganadores(t), g 6= u ] ; asegura otrosParticipantesMantienenEstado : (∀p ← participantes(result))puntajeAcumulado(result, p) == puntajeAcumulado(t, p) ∧ (p ∈ / ganadores(result) → proxP regunta(result, p) == proxP regunta(t, p)) ; } problema procesarRespuestaT (t: Trivia, u: Usuario, r: Texto) = result : (Trivia,SMS) { requiere estaRegistrado : u ∈ participantes(t) ; asegura seMantienenKeywords : mismos(keywords(prm(result)), keywords(t)) ; asegura seMantienenPreguntas : preguntas(prm(result)) == preguntas(t) ; asegura seMantienenParticipante : mismos(participantes(prm(result)), participantes(t)) ; asegura siTerminoEsGanador : leF altaResponderSoloU na(t, u) → ganadores(prm(result)) == ganadores(t) + +[u] ; asegura siNoTerminoNoEsGanador : ¬leF altaResponderSoloU na(t, u) → ganadores(prm(result)) == ganadores(t) ; asegura otrosParticipantesMantienenEstado : (∀p ← participantes(t), p 6= u)puntajeAcumulado((prm(result), p) == puntajeAcumulado(t, p) ∧ (p ∈ / ganadores(t) → proxP regunta((prm(result), p) == proxP regunta(t, p)) ; asegura avanzaUnaPregunta : leF altaResponderV arias(t, u) → proxP regunta(prm(result), u) == preguntas(prm(result))indiceP reg(t,u)+1 ; asegura actualizaPuntaje : (u ∈ ganadores(t) → puntajeAcumulado(prm(result), u) == puntajeAcumulado(t, u)) ∧ (u ∈ / ganadores(t) → puntajeAcumulado(prm(result), u) == puntajeAcumulado(t, u) + puntosQueSuma(t, u, r)) ; asegura laRespuestaLeLlega : nroDestino(sgd(result)) == u ; asegura textoSiTermino : leF altaResponderSoloU na(t, u) → esM ensajeF inal(sgd(result), prm(result), u) ; asegura textoSiNoTermino : leF altaResponderV arias(t, u) → esM ensajeP roximaP regunta(r, sgd(result), prm(result), u) ; asegura textoSiYaHabiaGanado : u ∈ ganadores(t) → esM ensajeDeSeguiP agando(sgd(result), u) ; } problema usuariosEficientesT (t: Trivia) = result : [Usuario] { asegura mismos(result, losQueM enosM andaron(t, losQueM asP untosT ienen(t))) ; } problema posicionEnT (t: Trivia, u: Usuario) = result : Z { requiere estaRegistrado : u ∈ participantes(t) ; asegura result == posicionEnT rivia(t, u) ; } problema palabrasRecurrentesT (t: Trivia, n: Z) = result : [String] { asegura mismos(result, sacarRepetidos(soloM ayoresAN (n, lasM asRecurrentes(concat([palabras(texto(p)) + +palabras(rtaCorrecta(p))|p ← preguntas(t)])))) ; }

4

4.

Gateway

tipo Gateway observador observador observador invariante invariante invariante invariante

{ numero (g: Gateway) : Numero ; trivias (g: Gateway) : [Trivia] ; comandos (g: Gateway) : [Keyword] ; sinTriviasRepetidas : sinRepetidos(trivias(g)) ; sinComandosRepetidos : sinRepetidos(comandos(g)) ; noSeSuperponenTrivias : (∀t1 , t2 ← trivias(g), t1 6= t2 ) |interseccion(keywords(t1 ), keywords(t2 ))| == 0 ; noSeSolapanComandosConTrivias : (∀t ← trivias(g)) |interseccion(keywords(t), comandos(g))| == 0 ;

} problema nuevoG (n: Numero, cs: [Keyword]) = result : Gateway { requiere sinRepetidos(cs) ; asegura numero(result) == n ∧ mismos(comandos(result), cs) ∧ |trivias(result)| == 0 ; } problema numeroG (g: Gateway) = result : Numero { asegura result == numero(g) ; } problema triviasG (g: Gateway) = result : [Trivia] { asegura mismos(result, trivias(g)) ; } problema comandosG (g: Gateway) = result : [Keyword] { asegura mismos(result, comandos(g)) ; } problema agregarTriviaG (t: Trivia, g: Gateway) = result : Gateway { requiere noRepiteKeyword : (∀x ← trivias(g)) |interseccion(keywords(t), keywords(x))| == 0 ; requiere noTieneKeywordQueEsComando : |interseccion(keywords(t), comandos(g))| == 0 ; asegura mantieneNroYComandos : numero(result) == numero(g) ∧ mismos(comandos(result), comandos(g)) ; asegura seAgregaTrivia : mismos(trivias(result), t : trivias(g)) ; } problema procesarComandoG (g: Gateway, u: Usuario, s: SMS) = result : (Gateway, SMS) { requiere esParticipanteDeAlguna : (∃t ← trivias(g))u ∈ participantes(t) ; requiere esUnMensajeParaMi : nroDestino(s) == numero(g) ; asegura noEntiendoElComando : ¬esComando(texto(s), g) → g == prm(result)∧esM ensajeN oT eEntiendo(sgd(result), u) ; asegura noEntiendoLaKeyword : (esComando(texto(s), g) ∧ comandoConKeywordInvalida(texto(s), trivias(g), u)) → g == prm(result) ∧ esM ensajeN oT eEntiendo(sgd(result), u) ; asegura numeroComandosYTriviasSiEsRanking : esComandoRanking(texto(s)) → g == prm(result) ; asegura mensajeSiEsRanking : esComandoRanking(texto(s)) → esM ensajeRanking(s, sgd(result), u, g) ; asegura numeroComandosYTriviasSiEsBaja : nuevoGwP osBaja(g, prm(result), obtenerKeywordDeComando(texto(s)), u) ; asegura mensajeSiEsBaja : esComandoBaja(texto(s)) → esM ensajeBaja(sgd(result), u) ; } problema procesarMensajeG (g: Gateway, u: Usuario, s: SMS) = result : (Gateway, SMS) { requiere noEsUnComando : ¬primerP alabraP ertenece(texto(s), comandos(g)) ; requiere esUnMensajeParaMi : nroDestino(s) == numero(g) ; asegura noEntiendo : noEsKeyword(texto(s), trivias(g)) → esM ensajeN oT eEntiendo(sgd(result), u) ; asegura nuevoJugador : ¬esJugador(u, g, s) → (nuevoGwConJugadorN uevo(g, prm(result), extraerKeywordSM S(s), u) ∧ esM ensajeP rimerP regunta(sgd(result), triviaXKeyword(trivias(prm(result)), extraerKeywordSM S(s)), u)) ; asegura yaEraGanador : esJugadorGanador(u, g, s) → (g == prm(result) ∧ esM ensajeDeSeguiP agando(sgd(result), u)) ; asegura estaPorGanar : esJugadorY LeF altaU na(u, g, s) → (nuevoGwConN uevoGanador(g, prm(result), s, u) ∧ esM ensajeF inal(sgd(result), triviaXKeyword(trivias(prm(result)), extraerKeywordSM S(s)), u)) ; asegura sigueJugando : esJugadorLeF altanV arias(u, g, s) → (nuevoGwSinN uevoGanador(g, prm(result), s, u) ∧ esM ensajeP roximaP regunta(triviaXKeyword(trivias(g), extraerKeywordSM S(s)), texto(s), sgd(result), u, triviaXKeyword(trivias(prm(result)), extraerKeywordSM S(s)))) ;

5

} problema seAnotanEnTodasG (g: Gateway) = result : [Usuario] { asegura mismos(result, [u|u ← todosLosU suarios(g), seAnotoEnT odas(g, u) ∧ terminoAlguna(g, u)]) ; }

5.

Telco

tipo TelCO { observador usuarios (t: TelCO) : [Usuario] ; observador gateways (t: TelCO) : [Gateway] ; observador mensajes (t: TelCO, u: Usuario) : [(SMS, SMS)] ; requiere u ∈ usuarios(t) ; invariante usuariosDistintos : sinRepetidos(usuarios(t)) ; invariante noHayGatewaysRepetidos : sinRepetidos([numero(g)|g ← gateways(t)]) ; invariante smsEnviadosValidos : (∀u ← usuarios(t))(∀m ← mensajes(t, u)) hayGatewayConN ro(nroDestino(prm(m)), gateways(t)) ; invariante smsRecibidosValidos : (∀u ← usuarios(t))(∀m ← mensajes(t, u))nroDestino(sgd(m)) == u ; } problema nuevoTE (gs: [Gateway]) = result : TelCO { asegura sinUsuarios : usuarios(result) == [] ; asegura conGateways : mismos(gateways(result), gs) ; } problema usuariosTE (t: TelCO) = result : [Usuario] { asegura mismos(result, usuarios(t)) ; } problema esNroDeGatewayTE (t: TelCO, n: Numero) = result : Bool { asegura result == (∃g ← gateways(t))numero(g) == n ; } problema gatewayTE (t: TelCO, n: Numero) = result : Gateway { requiere esNroDeAlgunGateway : (∃g ← gateways(t))numero(g) == n ; asegura result == gatewayXN ro(t, n) ; } problema mensajesTE (t: TelCO, u: Usuario) = result : [(SMS, SMS)] { requiere esUsuario : u ∈ usuarios(t) ; asegura result == mensajes(t, u) ; } problema agregarUsuarioTE (t: TelCO, u: Usuario) = result : TelCO { requiere noEsUsuario : u ∈ / usuarios(t) ; asegura nuevoUsuario : mismos(u : usuarios(t), usuarios(result)) ; asegura mismosGateways : mismos(gateways(t), gateways(result)) ; asegura mismosMensajes : (∀x ← usuarios(t))mensajes(t, x) == mensajes(result, x) ; asegura elNuevoNoTieneMensajes : mensajes(result, u) == [] ; } problema procesarMensajeTE (t: TelCO, u: Usuario, sms: SMS) = result : Telco { requiere esUsuario : u ∈ usuarios(t) ; requiere existeGatewayDestino : (∃g ← gateways(t))numero(g) == nroDestino(sms) ; asegura seMantienenLosUsuarios : mismos(usuarios(t), usuarios(result)) ; asegura mismosMensajesDeOtros : (∀x ← usuarios(result), x 6= u)mensajes(t, x) == mensajes(result, u) ; asegura hayUnMensajeNuevo : |mensajes(t, u)| == |mensajes(result, u)| − 1 ; asegura mismosMensajesViejos : mensajes(t, u) == mensajes(result, u)[0..|mensajes(result, u)| − 1) ; asegura losOtrosGatewaysNoCambian : mismos(sacarGateway(gateways(t), gatewayXN ro(t, n)), sacarGateway(gateways(result), gatewayXN ro(result, n))) ; asegura cambiosEnGateway : (∃g ← gateways(g), numero(g) == nroDestino(sms)) (∃r ← gateways(result), numero(g) == nroDestino(sms)) (gatewayDespuesDeP rocesarM ensaje(g, r, sms, u, ultimo(mensajes(result)))) ;

6

} problema infoGatewaysTE (t: TelCO) = result : [(Gateway, Z, Z)] { asegura infoCorrecta : mismos(result, [(g, |trivias(g)| , cuantosJueganAlgunaT rivia(t, g))|g ← gateways(t)]) ; asegura infoOrdenada : (∀i ← [0.. |result| − 1))trc(result)i ≥ trc(result)i+1 ; }

7

6.

Funciones Auxiliares

7.

Auxiliares

7.1.

B

aux bienOMal (t: Trivia, u: Usuario, r: Texto) : Texto = if rtaCorrecta(proxP regunta(t, u)) == sacarP rimerP alabra(r) then ”Bien!” else ”M al!” ;

7.2.

C

aux cantAp (x:T, xs:[T]) : Z = |[1|y ← xs, x == y]| ; aux comandoConKeywordInvalida (s: String, ts: [Trivia], u: Usuario) : Bool = (esComandoRanking(s) ∨ esComandoBaja(s)) ∧ (noEncuentraT rivia(segundaP alabra(s), ts) ∨ ¬elU suarioEstaEnEsaT rivia(segundaP alabra(s), ts, u)) ; aux cuantosJueganAlgunaTrivia (t: TelCO, g: Gateway) : Z = |[u|u ← usuarios(t), (∃x ← trivias(g))u ∈ participantes(x)]| ;

7.3.

E

aux esComando (s: String, g: Gateway) : Bool = (primerP alabraP ertenece(texto(s), comandos(g))) ∧ (esComandoRanking(texto(s)) ∨ esComandoBaja(texto(s))) ; aux esComandoBaja (t: String) : Bool = extraerComando(t) == ”BAJA” ; aux esComandoRanking (t: String) : Bool = extraerComando(t) == ”RAN KIN G” ; aux esJugador (u: Usuario, g: Gateway, s: SMS) : Bool = u ∈ participantes(triviaXKeyword(trivias(g), extraerKeywordSM S(s))) ; aux esJugadorGanador (u: Usuario, g: Gateway, s: SMS) : Bool = u ∈ participantes(triviaXKeyword(trivias(g), extraerKeywordSM S(s))) ∧ u ∈ ganadores(triviaXKeyword(trivias(g), extraerKeywordSM S(s))) ; aux esJugadorLeFaltanVarias (u: Usuario, g: Gateway, s: SMS) : Bool = u ∈ participantes(triviaXKeyword(trivias(g), extraerKeywordSM S(s))) ∧ leF altaResponderV arias(triviaXKeyword(trivias(g), extraerKeywordSM S(s)), u) ; aux esJugadorYLeFaltaUna (u: Usuario, g: Gateway, s: SMS) : Bool = u ∈ participantes(triviaXKeyword(trivias(g), extraerKeywordSM S(s)))∧ leF altaResponderSoloU na(triviaXKeyword(trivias(g), extraerKeywordSM S(s)), u) ; aux esMensajeBaja (s: SMS, u: Usuario) : Bool = nroDestino(s) == u ∧ texto(s) == ”Listo, ya te borramos” ; aux esMensajeDeSeguiPagando (s: SMS, u: Usuario) : Bool = nroDestino(s) == u∧texto(s) == ”Gracias por seguir pagando pero el juego termino” ; aux esMensajeFinal (s: SMS, t: Trivia, u: Usuario) : Bool = nroDestino(s) == u ∧ texto(s) == ”Has respondido todas las preguntas. ” + +textoP untaje(t, u) ; aux esMensajeNoTeEntiendo (s: SMS, u: Usuario) : Bool = nroDestino(s) == u ∧ texto(s) == ”No te entiendo” ; aux esMensajePrimerPregunta (s: SMS, t: Trivia, u: Usuario) : Bool = nroDestino(s) == u ∧ texto(s) == ”Hola! Tenes 0 pts” + +texto(preguntas(t)0 ) ; aux esMensajeProximaPregunta (o: Trivia, r: String, s: SMS, u: Usuario, t: Trivia) : Bool = nroDestino(s) == u ∧ texto(s) == bienOM al(o, u, r) + +textoP untaje(t, u) + +texto(proxP regunta(t, u)) ; aux esMensajeRanking (smsOrig, smsRta: SMS, u: Usuario, g: Gateway) : Bool = nroDestino(smsRta) == u ∧ (∃t ← trivias(g), keywordDeComando(texto(smsOrig)) ∈ keywords(t)) texto(smsRta) == ”Tu posicion es: ” + +intT oString(posicionEnT rivia(t, u) ; aux elUsuarioEstaEnEsaTrivia (k: String, ts: [Trivia], u: Usuario) : Bool = (∀t ← ts, k ∈ keywords(t))u ∈ participantes(t) ; aux extraerComando (t: String) : Keyword = primerP alabra(quitarEspacios(t)) ; aux extraerComandoDeSMS (s: SMS) : Keyword = primerP alabra(quitarEspacios(texto(s))) ; aux extraerKeyword (s: String) : Keyword = primerP alabra(quitarEspacios(s)) ; aux extraerKeywordSMS (s: SMS) : Keyword = primerP alabra(quitarEspacios(texto(s))) ;

7.4.

G

aux gatewayDespuesDeBaja (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS, SMS)) : Bool = (extraerComandoSM S(s) ∈ comandos(original) ∧ esComandoBaja(texto(s))) → (nuevoGwP osBaja(original, nuevo, obtenerKeywordDeComando(texto(sms)), usr)f ∧ prm(ms) == sms ∧ esM ensajeBaja(sgd(ms), usr)) ; aux gatewayDespuesDeComando (original: Gateway, nuevo: Gateway, s: SMS, u: Usuario, ms: (SMS, SMS)) : Bool = gatewayDespuesDeRanking(original, nuevo, s, u, ms) ∧ gatewayDespuesDeBaja(original, nuevo, s, u, ms) ∧ gatewayDespuesDeOtroComando(original, nuevo, s, u, ms) ; aux gatewayDespuesDeKeywordInvalida (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS,SMS)) : Bool = (¬primerP alabraP ertenece(texto(sms), comandos(g)) ∧ noEsKeyword(texto(sms), trivias(original)) → (original == nuevo ∧ esM ensajeN oT eEntiendo(sgd(ms), usr) ∧ prm(ms) == sms) ;

8

aux gatewayDespuesDeKeywordYJugadorGanador (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS,SMS)) : Bool = (¬primerP alabraP ertenece(texto(sms), comandos(g)) ∧ esJugadorGanador(usr, orginal, sms)) → (original == nuevo ∧ prm(ms) == sms ∧ esM ensajeDeSeguiP agando(sgd(ms), usr)) ; aux gatewayDespuesDeKeywordYJugadorNuevo (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS,SMS)) : Bool = (¬primerP alabraP ertenece(texto(sms), comandos(g)) ∧ ¬esJugador(usr, orginal, sms)) → (nuevoGwConJugadorN uevo(original, nuevo, extraerKeywordSM S(sms), usr) ∧ prm(ms) == sms ∧ esM ensajeP rimerP regunta(sgd(ms), triviaXKeyword(trivias(nuevo), extraerKeyword(s)), usr)) ; aux gatewayDespuesDeKeywordYJugadorNuevoGanador (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS,SMS)) : Bool = (¬primerP alabraP ertenece(texto(sms), comandos(g)) ∧ ¬esJugadorY LeF altaU na(usr, orginal, sms)) → (nuevoGwConN uevoGanador(original, nuevo, sms, usr) ∧ prm(ms) == sms ∧ esM ensajeF inal(texto(sms), sgd(ms), triviaXKeyword(trivias(nuevo), extraerKeywordSM S(sms)), usr)) ;

aux gatewayDespuesDeKeywordSinGanador (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS,SMS)) : Bool = (¬primerP alabraP ertenece(texto(sms), comandos(g)) ∧ ¬esJugadorLeF altanV arias(usr, orginal, sms)) → (nuevoGwSinN uevoGanador(original, nuevo, sms, usr) ∧ prm(ms) == sms∧esM ensajeP roximaP regunta(triviaXKeyword(trivias(original), extraerKeywordSM S(sms)), texto(sms), sgd(ms), usr, triviaX aux gatewayDespuesDeOtroComando (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS, SMS)) : Bool = (¬esComando(texto(sms), original) ∨ comandoConKeywordInvalida(texto(sms), trivias(original), u)) → (original == nuevo ∧ esM ensajeN oT eEntiendo(sgd(ms), usr) ∧ prm(ms) == sms) ; aux gatewayDespuesDeProcesarMensaje (original: Gateway, nuevo: Gateway, s: SMS, u: Usuario, ms: (SMS, SMS)) : Bool = gatewayDespuesDeComando(original, nuevo, s, u, ms) ∧ gatewayDespuesDeKeywordInvalida(original, nuevo, s, u, ms) ∧ gatewayDespuesDeKeywordY JugadorN uevo(original, nuevo, s, u, ms) ∧ gatewayDespuesDeKeywordY JugadorGanador(original, nuevo, s, u, ms) ∧ gatewayDespuesDeKeywordY JugadorN uevoGanador(original, nuevo, s, u, ms) ∧ gatewayDespuesDeKeywordSinGanador(original, nuevo, s, u, ms) ; aux gatewayDespuesDeRanking (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario, ms: (SMS, SMS)) : Bool = (extraerComandoSM S(sms) ∈ comandos(original) ∧ esComandoRanking(texto(sms))) → (original == nuevo ∧ prm(ms) == sms ∧ esM ensajeRanking(s, sgd(ms), usr, nuevo)) ; aux gatewayXNro (t: TelCO, n: Numero) : Gateway = [g|g ← gateways(t), numero(g) == n]0 ;

7.5.

H

aux hayGatewayConNro (nro:Z, gs: [Gateway]) : Bool = (∃g ← gs)numero(g) == nro ;

7.6.

I

aux igualesConNuevoGanador (t: Trivia, r: Trivia, u: Usuario, x: String) : Bool = mismos(keywords(t), keywords(r)) ∧ preguntas(t) == preguntas(r) ∧ mismos(participantes(t), participantes(r)) ∧ ganadores(t) + +[u] == ganadores(r) ∧ (∀k ← participantes(r), k 6= u)puntajeAcumulado(r, k) == puntajeAcumulado(t, k) ∧ (∀k ← participantes(r), k 6= u ∧ k ∈ / ganadores(r))proximaP regunta(r, k) == proximaP regunta(t, k) ∧ puntajeAcumulado(r, u) == puntajeAcumulado(t, u) + puntosQueSuma(t, u, x) ; aux igualesConNuevoPuntaje (t: Trivia, r: Trivia, u: Usuario, x: String) : Bool = mismos(keywords(t), keywords(r)) ∧ preguntas(t) == preguntas(r) ∧ mismos(participantes(t), participantes(r)) ∧ ganadores(t) == ganadores(r) ∧ (∀k ← participantes(r), k 6= u)puntajeAcumulado(r, k) == puntajeAcumulado(t, k) ∧ (∀k ← participantes(r), k 6= u ∧ k ∈ / ganadores(r))proximaP regunta(r, k) == proximaP regunta(t, k) ∧ puntajeAcumulado(r, u) == puntajeAcumulado(t, u) + puntosQueSuma(t, u, x) ∧ proxP regunta(r, u) == preguntas(r))indiceP reg(t,u)+1 ; aux igualesSalvoUsuario (t: Trivia, r: Trivia, u: Usuario) : Bool = mismos(keywords(t), keywords(r)) ∧ preguntas(t) == preguntas(r) ∧ mismos(participantes(t), u : participantes(r)) ∧ sacarU suario(ganadores(t), u) == ganadores(r) ∧ (∀k ← participantes(r))puntajeAcumulado(r, k) == puntajeAcumulado(t, k) ∧ (∀k ← participantes(r), k ∈ / ganadores(r))proximaP regunta(r, k) == proximaP regunta(t, k) ; aux igualesConUsuario (t: Trivia, r: Trivia, u: Usuario) : Bool = mismos(keywords(t), keywords(r)) ∧ preguntas(t) == preguntas(r) ∧ mismos(u : participantes(t), participantes(r)) ∧ ganadores(t) == ganadores(r) ∧ (∀k ← participantes(t))puntajeAcumulado(r, k) == puntajeAcumulado(t, k) ∧ (∀k ← participantes(t), k ∈ / ganadores(t))proximaP regunta(r, k) == proximaP regunta(t, k) ∧ puntajeAcumulado(r, u) == 0 ∧ proximaP regunta(r, u) == preguntas(r)0 ; aux indiceEnGanadores (u: Usuario, t: Trivia) : Z = [i|i ← [0..|ganadores(t)), ganadores(t)i == u]0 ; aux indicePreg (t: Trivia, u: Usuario) : Z = [i|i ← [0.. |preguntas(t)|), preguntas(t)i == proxP regunta(t, u)]0 ; aux interseccion (a, b: [T]) : [T] = [x|x ← a, x ∈ b] ;

7.7.

L

aux lasMasRecurrentes (xs:[String]) : [String] = [x|x ← xs, (∀y ← xs)cantAp(y, xs) ≤ cantAp(x, xs) ; aux leFaltaResponderSoloUna (t: Trivia, u: Usuario) : Bool = u∈ / ganadores(t) ∧ proxP regunta(t, u) == ultimo(preguntas(t)) ; aux leFaltaResponderVarias (t: Trivia, u: Usuario) : Bool = u∈ / ganadores(t) ∧ proxP regunta(t, u) 6= ultimo(preguntas(t)) ;

9

aux losQueMasPuntosTienen (t: Trivia) : [Usuario] = [u|u ← participante(t), tieneM asP untosQueT odos(t, u)] ; aux losQueMenosMandaron (t: Trivia, us: [Usuario]) : [Usuario] = [u|u ← us, mandoM enosQueLosDemas(t, u, us)] ;

7.8.

M

aux mandoMenosQueLosDemas (t: Trivia, u: Usuario, us: [Usuario]) : Bool = (∀p ← us)indiceP reg(t, u) ≤ indiceP reg(t, p) ;

7.9.

N

aux noEncuentraTrivia (k: String, ts: [Trivia]) : Bool = (∀t ← ts)k ∈ / keywords(t) ; aux noEsKeyword (k: String, ts: [Trivia]) : Bool = noEncuentraT rivia(primerP alabra(quitarEspacios(s)), ts) ; – Deprecada

aux noEsTriviaDelUsuario (ts: [Trivia], u: Usuario) : Bool = (∀t ← ts)u ∈ / participantes(t) ;

aux nuevoGwConJugadorNuevo (original: Gateway, nuevo: Gateway, key: Keyword, usr: Usuario) : Bool = (|trivias(original)| == |trivias(nuevo)|) ∧ mismos(triviasDeOtrasKeywords(key, original), triviasDeOtrasKeywords(key, trivias(nuevo))) ∧ (∃t ← trivias(original), key ∈ keywords(t))(∃r ← trivias(nuevo), key ∈ keywords(r))(igualesConU suario(t, r, usr)) ∧ numero(original), numero(nuevo) ∧ mismos(comandos(original), comandos(nuevo)) ; aux nuevoGwConNuevoGanador (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario) : Bool = (|trivias(original)| == |trivias(nuevo)|) ∧ mismos(triviasDeOtrasKeywords(extraerKeywordSM S(sms), trivias(original)), triviasDeOtrasKeywords(extraerKeywordSM S(sms), trivias(nuevo))) ∧ (∃t ← trivias(original), extraerKeywordSM S(sms) ∈ keywords(t))(∃r ← trivias(nuevo), extraerKeywordSM S(sms) ∈ keywords(r)) (igualesConN uevoGanador(t, r, usr, texto(sms)) ∧ numero(original) == numero(nuevo) ∧ mismos(comandos(original), comandos(nuevo))) ; aux nuevoGwPosBaja (original: Gateway, nuevo: Gateway, key: Keyword, usr: Usuario) : Bool = (|trivias(original)| == |trivias(nuevo)|) ∧ mismos(triviasDeOtrasKeywords(key, original), triviasDeOtrasKeywords(key, trivias(nuevo))) ∧ (∃t ← trivias(original), key ∈ keywords(t))(∃r ← trivias(nuevo), key ∈ keywords(r))igualesSalvoU suario(t, r, usr) ∧ numero(original) == numero(nuevo) ∧ mismos(comandos(original), comandos(nuevo)) ; aux nuevoGwSinNuevoGanador (original: Gateway, nuevo: Gateway, sms: SMS, usr: Usuario) : Bool = (|trivias(original)| == |trivias(nuevo)|) ∧ mismos(triviasDeOtrasKeywords(extraerKeywordSM S(sms), trivias(original)), triviasDeOtrasKeywords(extraerKeywordSM S(sms), trivias(nuevo))) ∧ (∃t ← trivias(original), extraerKeywordSM S(sms) ∈ keywords(t))(∃r ← trivias(nuevo), extraerKeywordSM S(sms) ∈ keywords(r)) (igualesConN uevoP untaje(t, r, usr, texto(sms)) ∧ numero(original) == numero(nuevo) ∧ mismos(comandos(original), comandos(nuevo))) ;

7.10.

P

aux primerPalabra (t: String) : String = [ti |i ← [0..|t|),’ ’∈ / t[0..i) ∧ ti 6=’ ’] ; aux primerPalabraPertenece (t: String, cs: [Keyword]) : Bool = primerP alabra(quitarEspacios(t)) ∈ cs ; aux posicionEnTrivia (t: Trivia,u: Usuario) : Z = if u ∈ ganadores(t) then indiceEnGanadores(u, t) else |ganadores(t)|+|tienenM asP untos(t, u)| ; aux puntosQueSuma (t: Trivia, u: Usuario, r: Texto) : Z = puntaje(proxP regunta(t, u)) ∗ β(rtaCorrecta(proxP regunta(t, u)) == sacarP rimerP alabra(r)) ;

7.11.

O

aux obtenerKeywordDeComando (t: String) : Keyword = segundaP alabra(quitarEspacios(t)) ;

7.12.

Q

aux quitarEspacios (t: String) : String = [xi |i ← [0..|t|), xi 6=’ ’] ;

7.13.

S

aux sacarPrimerPalabra (t: String) : String = [ti |i ← (|primerP alabra(t)|..|t|)] ; aux sacarRepetidos (a: [T]) : [T] = [ai |i ← [0.. |a|), ai ∈ / a[0..i)] ; aux sacarUsuario (us: [Usuario], u: Usuario) : [Usuario] = [x|x ← us, x 6= u] ; aux seAnotoEnTodas (g: Gateway, u: Usuario) : Bool = (∀t ← trivias(g))u ∈ participantes(t) ; aux segundaPalabra (t: String) : String = primerP alabra(sacarP rimerP alabra(t)) ; aux soloMayoresAN (n:Z, xs: [String]) : [String] = [x|x ← xs, |x| ≥ n] ; aux sinRepetidos (a: [T]) : Bool = (∀i, j ← [0..|a|), i 6= j)ai 6= aj ;

10

7.14.

T

aux terminoAlguna (g: Gateway, u: Usuario) : Bool = (∃t ← trivias(g))u ∈ ganadores(t) ; aux textoPuntaje (t: Trivia, u: Usuario) : Texto = ”T enes” + +puntajeAcumulado(t, u) + +”pts.” ; aux tieneMasPuntosQueTodos (t: Trivia, u: Usuario) : Bool = (∀p ← participantes(t))puntajeAcumulado(t, u) ≥ puntajeAcumulado(t, p) ; aux tienenMasPuntos (t: Trivia, u: Usuario) : [Usuario] = [p|p ← participantes(t), p ∈ / ganadores(t) ∧ puntajeAcumulado(t, p) > puntajeAcumulado(t, u)] ; aux todosLosUsuarios (g: Gateway) : [Usuario] = sacarRepetidos([u|t ← trivias(g), u ← participantes(t)]) ; aux triviasDeOtrasKeywords (k: String, ts: [Trivia]) : [Trivia] = [t|t ← ts, k ∈ / keywords(t)] ; aux triviaXKeyword (ts: [Trivia], k: String) : Trivia = [x|x ← ts, k ∈ keywords(x)]0 ;

7.15.

U

aux ultimo (a: [T]) : T = a|a|−1 ;

11