problema 25 ........ separado del resto.

1er post(eze

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. 

2do post (mariano)

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

3er post (eze)


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. 


4to post (eze)

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.


5to post (eze)


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


6to post (eze)


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


7mo post (mariano)

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.