Zadanie 1
Misjonarze i ludzożercy
- Po jednej stronie rzeki znajduje się 3 misjonarzy i 3 ludzożerców.
- Jest łódka, która może pomieścić maksymalnie 2 osoby. Łódką zawsze musi płynąć co najmniej jedna osoba.
- Cel: Przeprawić wszystkich na drugą stronę tak, aby w żadnym momencie na jednej stronie rzeki ludożercy nie przewyższali liczebnie misjonarzy.
Zadanie 2
Wilk, koza i kapusta
- Po jednej stronie rzeki znajdują się wilk, koza i kapusta, towarzyszy im wieśniak.
- Ma za zadanie przewieźć ich wszystkich na drugą stronę rzeki, ale jednocześnie może pomieścić tylko jeden z tych bytów.
- Wilk pozostawiony bez nadzoru zje kozę, a koza zje kapustę.
Zadanie 3
Modelujemy ruch pociągów.
- Tory składają się z „odcinków”. Modelować je będziemy poprzez zbiór Segment, wyposażony w relację next, która mówi o tym jak łączą się ze sobą poszczególne odcinki.
- Do zderzenia pociągów może dojść wtedy i tylko wtedy, gdy znajdą się jednocześnie na jednym odcinku toru. Pociągi modelować będziemy poprzez zbiór Train. Dynamiczny stan pociągu opisany jest poprzez zbiór TrainState, wyposażony w relację on, która każdemu pociągowi przypisuje (jedyny) odcinek toru, na którym się on (w danej chwili) znajduje. Zbiór TrainState wyposażymy dodatkowo w informację o zbiorze wszystkich odcinków torów, które w bieżącym stanie są zajęte – nazwijmy ją occupied.
- Do opisu przemieszczania się pociągów użyjemy predykatu, który jako argumenty brać będzie dwa stany (przed i po wykonaniu „ruchu”) oraz zbiór pociągów, które biorą udział w danym ruchu. Każdy z pociągów przemieszcza się oczywiście zgodnie z relacją next dla odcinka toru, na którym się znajduje.
- System bezpieczeństwa składać się będzie z semaforów. Mówią one o tym, czy dany odcinek jest „zamknięty”, czy też nie. Stan ustawienia semaforów modelować będziemy za pomocą zbioru GateState, z relacją closed opisującą zamknięte odcinki. Zasadę działania systemu semaforów opiszemy za pomocą predykatu charakteryzującego „dozwolone ruchy” pociągów. Predykat ten może np. mieć trzy argumenty: GateState, TrainState oraz zbiór pociągów, które bierzemy pod uwagę.
- Aby zdefiniować „politykę bezpieczeństwa” należy wprowadzić predykat, którego argumentami będą GateState i TrainState. Predykat ten powinien wymuszać sensowne „minimalne” warunki dotyczące bezpieczeństwa – np. „jeśli kilka zajętych odcinków torów ma wspólny następnik, to dla co najwyżej jednego powinien być otwarty semafor zezwalajacy na wjazd”...
- Na koniec należy sprawdzić, czy przy założeniu polityki bezpieczeństwa oraz wykonywaniu jedynie legalnych ruchów pociągów nie występują kolizje (tzn. nie ma możliwości przejścia od stanu bezpiecznego – do stanu, w którym dwa pociągi znajdą się na wspólnym odcinku toru).
Omawiane rozwiązanie NIE korzysta z możliwości użycia logiki temporalnej dostępnej w obecnej wersji Alloy'a. Warto rozważyć możliwość wykorzystania tej możliwości.