Abstract. Model finders are very popular for exploring scenarios, helping users validate specifications by navigating through conforming model instances. To be practical, the semantics of such scenario exploration operations should be formally defined and, ideally, controlled by the user, so that she is able to quickly reach interesting scenarios. This work explores the landscape of scenario exploration operations, by formalizing them with a relational model finder. Several scenario exploration operations provided by existing tools are formalized, and new ones are proposed, namely to allow the user to easily explore very similar (or different) scenarios, by attaching preferences to model elements. As a proof-of-concept, such operations were implemented in the popular Alloy Analyzer, further increasing its usefulness for (user-guided) scenario exploration.

Keywords. Model finding, scenario exploration, model-driven engineering. 

Coffee session: at 1:45 PM, Auditorium A2, 1st Floor 
Talks session: at 2:00 PM, Auditorium A2, 1st Floor