Abstraction tool abstracts a state-space generated by Afra model checker by providing a list of variables. The output is an abstracted version of the input state space (we call the returned abstract model, Tiny Twin (TT)).
Input state space of a Timed Rebeca model (state dransition diagram): State-space file
List of variables: Variables
Abstracted version of the input state space (state dransition diagram): Tiny Twin