The repository contains the formalization in Alloy of task models in the HAMSTERS notation. It also contains the formalization of a concrete task model for an Arrival MANager (AMAN) interactive system. These models accompany the paper "Task Model Design and Analysis with Alloy", currently under revision.
It contains the following files:
HAMSTERS.als, the formalization of the structural and behavioral semantics of HAMSTERSAMAN.als, the specification of the AMAN task model and the composed interactive systemAMAN_fixed.als, a fixed version of AMAN to guarantee feedback and availabilityAMAN.thm, an Alloy custom theme to better visualize traces from the AMAN model