Mod 1 Todo Junto (a revisar)

17. problema agregarEtiqueta (e:Etiqueta, s:SA) = result:SA{
asegura result = = if(incluido(e,s)) then s else s++[e];

21.observador cantRepLista(l:ListadeReproducción, r: Reproductor) : Z;
requiere Incluido(e,archivos(r));

observador cantRepTema(t:Tema,r:Reproductor):Z;
requiere Incluido(t,archivos(r));

25.problema crearRep(s:SA)=result:Reproductor{
asegura archivos(result)= =s;
asegura estado(result) = = (0, listas(result));
}//No entiendo si eso es que el aparato esté en stop. Ni si requiere algo.

29.problema actual(r:Reproductor)=result:Tema{
requiere prm(estado(r))!=0;
asegura Incluido(result,archivos(r));//Pero como aseguro que es el actual?
}//Considero que si está en un número distinto de 0 es porque está reproduciendo un archivo, por lo que no tengo que requerir que archivos(r)!=[ ]?

33.problema temaContenidoEnMasListas(r:Reproductor)=result:Tema{
requiere archivos(r)!=[ ];
asegura Incluido(result,archivos(r));
asegura Mayor(SumaBin(listas(r),result),[SumaBin(x,listas(r)) | x ←archivos(r)]);
}

17. problema agregarEtiqueta (e:Etiqueta, s:SA) = result:SA{
asegura result = = if(incluido(e,s)) then s else s++[e];
// no podes comparar cosas de distinto tipo. ni siquiera concatenarlas.(mariano)

21.observador cantRepLista(l:ListadeReproducción, r: Reproductor) : Z;
requiere Incluido(e,archivos(r));
// estas comparando cosas que no se pueden comparar.

observador cantRepTema(t:Tema,r:Reproductor):Z;
requiere Incluido(t,archivos(r));
//lo mismo que arriba.

25.problema crearRep(s:SA)=result:Reproductor{
asegura archivos(result)= =s;
asegura estado(result) = = (0, listas(result));
}//No entiendo si eso es que el aparato esté en stop. Ni si requiere algo.
//aca tenes q crear un dato de tipo reproductor, por lo tanto tenes que definir cada uno de los observadores correctamente. y que lo q definiste cumpla con las invariantes

29.problema actual(r:Reproductor)=result:Tema{
requiere prm(estado(r))!=0;
asegura Incluido(result,archivos(r));//Pero como aseguro que es el actual?
}//Considero que si está en un número distinto de 0 es porque está reproduciendo un archivo, por lo que no tengo que requerir que archivos(r)!=[ ]?
//
33.problema temaContenidoEnMasListas(r:Reproductor)=result:Tema{
requiere archivos(r)!=[ ];// ARCHIVOS DE R DEVUELVE UN TIPO SA , no devuelve lista.
asegura Incluido(result,archivos(r));
asegura Mayor(SumaBin(listas(r),result),[SumaBin(x,listas(r)) | x ?archivos(r)]);// que carajo es sumabin? jejejjejeje.leelo entero el 6 (sigue del otro lado)
}

Hoy lo miré el tp y vi que había hecho muchas cosas sin entender, por eso que mezclaba algunas clases con otras y listas que iban con las que no. Sobre todo las etiquetas no las había terminado de entender. Y tenés razón, muchas veces me confundí con lo que devolvía archivos(r). Corregí lo que me pusiste en rojo y no sé si había algo más. Igual me quedaron algunas dudas sobre unas cosas que las puse como comentario.

17. problema agregarEtiqueta (e:Etiqueta, s:SA) = result:SA{
asegura etiquetas(result) = = if(pertenece(e,etiquetas(s))) then etiquetas(s) else etiquetas(s)++[e];// No me acuerdo bien como se usan los implica en vez del if.
asegura temas(result)= =temas(s);// no deberían de haber cambiado si solo agregué una etiqueta. En cuanto a los invariantes creo que no hay que decir nada, porque si la etiqueta ya estaba no la puse y si la puse es distinta. Y los temas son los mismos. Por lo tanto es un SA hecho y derecho.

aux pertenece(t:T,a:[T]) Bool=result= =(E t’←a))t’= =t;//Lo volví a definir, no lo encontré en los que anoté yo, no se pierde nada con rehacerlo.

21.observador cantRepLista(l:ListadeReproducción, r: Reproductor) : Z;
requiere pertenece(l,listas(r));

observador cantRepTema(t:Tema,r:Reproductor):Z;
requiere pertence(t,temas(archivos(r)));

25.problema crearRep(s:SA)=result:Reproductor{
requiere laListaDelEstadoEsUnaListaValida();
requiere elTemaActualEsUnTema();
requiere lasListasSonValidas();//Con Nico dijimos de hacer los invariantes como aux para después poder usarlos. Cuando estén definidos con parámetros los ponemos.
asegura archivos(result)= =s;
asegura estado(result) = = (0, listas(result));
asegura listas(r) = = [etiquetas(s)];
}//No entiendo si eso es que el aparato esté en stop. Sobre los otros dos observadores no sé que asegurar.

29.problema actual(r:Reproductor)=result:Tema{
requiere prm(estado(r))!=0;
asegura pertenece(result,temas(archivos(r)));//Pero como aseguro que es el actual?
}//Considero que si está en un número distinto de 0 es porque está reproduciendo un archivo, por lo que no tengo que requerir que archivos(r)!=[ ]?

33.problema temaContenidoEnMasListas(r:Reproductor)=result:Tema{
requiere temas(archivos(r))!=[ ];
asegura pertenece(result,temas(archivos(r)));
asegura Mayor(CuantasListas(result),[CuantasListas(t)| t ←temas(archivos((r))]);
}

aux CuantasListas(t:Tema) Z=result = =|etiquetas(t)|;
aux Mayor(a: Z ,b:[Z]) Bool = result = = (¥ x←b)a>=x;

25.problema crearRep(s:SA)=result:Reproductor{
requiere pertenece([],listas(result));
requiere laListaDelEstadoEsUnaListaValida();
requiere elTemaActualEsUnTema();
requiere lasListasSonValidas();//Con Nico dijimos de hacer los invariantes como aux para después poder usarlos. Cuando estén definidos con parámetros los ponemos.
asegura archivos(result)= =s;
asegura estado(result) = = (0,[]);//Sobre el cero tengo dudas, pero la [] indica detenido.
asegura listas(r) = = [etiquetas(s)];
}//Sobre los otros dos observadores no sé que asegurar.

25.problema crearRep(s:SA)=result:Reproductor{
requiere pertenece([],listas(result));
requiere laListaDelEstadoEsUnaListaValida();
requiere elTemaActualEsUnTema();
requiere lasListasSonValidas();//Con Nico dijimos de hacer los invariantes como aux para después poder usarlos. Cuando estén definidos con parámetros los ponemos.
asegura archivos(result)= =s;
asegura estado(result) = = (0,[]);//Sobre el cero tengo dudas, pero la [] indica detenido.
asegura listas(r) = = [etiquetas(s)];
asegura (V l <-- listas(result)) cantRepLista(l,r) = = 0;
asegura (V t <-- temas(archivos(result)) cantRepTema(t,r) = = 0;
}

Creo que habría que sacar lo de que requiere la lista vacia, por lo que entendí del que hizo el Admin de reproducir, la lista vacía no tiene que pertenecer a listas(r) para poder pasar por ese estado.

25.problema crearRep(s:SA)=result:Reproductor{
asegura archivos(result)= =s;
asegura estado(result) = = (0,[]);
asegura listas(r) = = [];
asegura (V l <-- listas(result)) cantRepLista(l,r) = = 0;
asegura (V t <-- temas(archivos(result)) cantRepTema(t,r) = = 0;
}

ACORDATE TODO LO QUE DIJO LA AYUDANTA SOBRE LOS INVARIANTES que solito el problema asegura los invaiantes. eliminada la duda del 0,0 es detenido.
listas(r) empieza vacia, despues iras agregando listas de reproducciones.