Prova Metodos Formais 2021_1

Prévia do material em texto

UNIVERSIDADE DE PERNAMBUCO
Escola Politécnica NOTA
Curso: Curso de Engenharia da Computação
Disciplina: Métodos Formais
Professor (a): Tarciana Dias da Silva
Exercício
Final
Turma: Data: 10/12/21
Nome do Aluno: Matrícula:
A T E N Ç Ã
O
1. Avaliação individual; cópias serão identificadas e terão pontuação
zerada, independentemente de quem copiou de quem.
1) Considere um sistema para compra de passagens aéreas, como, por exemplo,
decolar ou submarino. Ao fazer uma pesquisa num sistema como esse, você
pode se utilizar de filtros como, por exemplo, se você quer vôos diretos, com
apenas uma escala, 2 escalas, etc. Você também pode definir em qual
companhia aérea você quer voar, ou se tanto faz.
Certamente, tais sistemas possuem parcerias com sistemas de companhias
aéreas como GOL, AZUL, TAM, etc. Suponha que cada cia aérea disponibiliza à
decolar/submarino um conjunto de possíveis de vôos que podem ser oferecidos
aos clientes, exemplo:
VoosGol = {(Recife, Fortaleza), (Fortaleza, Belém), (Belém, Manaus)}
VoosAvianca = {(Recife, Brasilia), (Brasília, Manaus)}
Elabore um modelo Alloy que permita determinar e forneça elementos/restrições
para:
a) (1,5 pt) avaliar se determinada cidade pode ser utilizada como escala de
vôos disponíveis entre uma cidade origem e uma cidade destino
quaisquer; considere que apenas a cidade escala será passada como
parâmetro.
—-------------------------------------------
Considerando que como vôos parceiros das companhias Azul e Tam,
teríamos as seguintes listas abaixo:
VoosAzul={(Recife, Salvador), (São Paulo, Salvador), (Manaus,
Salvador), (Salvador, Curitiba)}
VoosTam={(Rio, Salvador), (Salvador, PortoAlegre) }
b) (1,5 pt) quantos e quais vôos seriam possíveis considerando a cidade de
Salvador como única escala?
c) (2 pts) elabore um predicado(s)/função que represente o dito na letra B
em Alloy. Novamente considere que apenas a cidade da escala será
fornecida como parâmetro.
d) (2 pt) elabore um predicado(s)/função que represente quantos vôos
(independentemente de serem diretos ou não) seriam possíveis
partindo-se de uma determinada cidade de origem, fornecida como
parâmetro.
e) (1 pt) Complemente a solução da letra D (caso ainda não o tenha feito)
que exclua os trechos que contenham indireção, ou seja, não deve ser
permitido que, partindo-se de uma determinada cidade você chegue nela
mesma;
f) (1 pt) acrescente no seu modelo uma forma de garantir que as relações
que representam os trechos aéreos das companhias aéreas são
simétricas
g) (1 pt) Defina através de uma única expressão em Alloy como
representaríamos todos os possíveis vôos (diretos ou não)
disponibilizados por uma companhia aérea (qualquer).