Bordeaux: A Tool for Thinking Outside the Box

  • Vajih MontaghamiEmail author
  • Derek Rayside
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


One of the great features of the Alloy Analyzer is that it can produce examples illustrating the meaning of the user’s model. These inside-the-box examples, which are formally permissible but (potentially) undesirable, help the user understand underconstraint bugs in the model. To get similar help with overconstraint bugs in the model the user needs to see examples that are desirable but formally excluded: that is, they need to see outside-the-box (near-miss) examples. We have developed a prototype extension of the Alloy Analyzer, named Bordeaux, that can find these examples that are near the border of what is permitted, and hence might be desirable. More generally, Bordeaux finds a pair of examples, ac, at a minimum distance to each other, and where a satisfies model A and c satisfies model C. The primary use case described is when model C is the negation of model A, but there are also other uses for this relative minimization. Previous works, such as Aluminum, have focused on finding inside-the-box examples that are absolutely minimal.


Model Transformation Alloy Model Unary Relation Alloy Analyzer Normal Logic Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



We thank Vijay Ganesh, Krzysztof Czarnecki, and Marsha Chechik for their helpful discussions. This work was funded in part by NSERC (National Science and Engineering Research Council of Canada).


  1. 1.
    Bak, K., Zayan, D., Czarnecki, K., Antkiewicz, M., Diskin, Z., Wasowski, A., Rayside, D.: Example-driven modeling: model = abstractions + examples. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, pp. 1273–1276. IEEE Press (2013)Google Scholar
  2. 2.
    Batot, E.: Generating examples for knowledge abstraction in MDE: a multi-objective framework. In: Balaban, M., Gogolla, M. (eds.) Proceedings of the ACM Student Research Competition at MODELS 2015 co-located with the ACM/IEEE 18th International Conference MODELS 2015, Ottawa, Canada, 29 September, 2015. CEUR Workshop Proceedings, vol. 1503, pp. 1–6 (2015).
  3. 3.
    Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial maxsat. AAAI/IAAI 263268 (1997)Google Scholar
  4. 4.
    Cunha, A., Macedo, N., Guimarães, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 17–31. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54804-8_2 CrossRefGoogle Scholar
  5. 5.
    Edwards, J., Jackson, D., Torlak, E.: A type system for object models. In: Taylor, R.N., Dwyer, M.B. (eds.) Proceedings of the \(12^{th}\) ACM/SIGSOFT International Symposium on the Foundations of Software Engineering (FSE). Newport Beach, CA, USA, November 2004Google Scholar
  6. 6.
    Gick, M.L., Paterson, K.: Do contrasting examples facilitate schema acquisition and analogical transfer? Can. J. Psychol./Rev. Can. Psychol. 46(4), 539 (1992)Google Scholar
  7. 7.
    Macedo, N., Cunha, A.: Implementing QVT-R bidirectional model transformations using Alloy. In: Cortellessa, V., Varró, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 297–311. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37057-1_22 CrossRefGoogle Scholar
  8. 8.
    Mendel, L.: Modeling by example. Master’s thesis, Massachusetts Institute of Technology, September 2007Google Scholar
  9. 9.
    Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: Proceedings of the 37th International Conference on Software Engineering - vol. 1, pp. 609–619. ICSE 2015, IEEE Press (2015)Google Scholar
  10. 10.
    Montaghami, V., Odunayo, O., Guntoori, B., Rayside, D.: Bordeaux prototype (2016).
  11. 11.
    Montaghami, V., Rayside, D.: Pattern-based debugging of declarative models. In: 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 322–327. IEEE (2015)Google Scholar
  12. 12.
    Mottu, J.-M., Baudry, B., Traon, Y.: Mutation analysis testing for model transformations. In: Rensink, A., Warmer, J. (eds.) ECMDA-FA 2006. LNCS, vol. 4066, pp. 376–390. Springer, Heidelberg (2006). doi: 10.1007/11787044_28 CrossRefGoogle Scholar
  13. 13.
    Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: Cheng, B., Pohl, K. (eds.) Proceedings of the \(35^{th}\) ACM/IEEE International Conference on Software Engineering (ICSE), San Francisco, CA, pp. 232–241 (2013)Google Scholar
  14. 14.
    Newcombe, C.: Debugging designs using exhaustively testable pseudo-code. Amazon Web Services (2011). Presentation Slides
  15. 15.
    Popelínský, L.: Efficient relational learning from sparse data. In: Scott, D. (ed.) AIMSA 2002. LNCS (LNAI), vol. 2443, pp. 11–20. Springer, Heidelberg (2002). doi: 10.1007/3-540-46148-5_2 CrossRefGoogle Scholar
  16. 16.
    Rosner, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F.: ParAlloy: towards a framework for efficient parallel analysis of alloy models. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 396–397. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-11811-1_33 CrossRefGoogle Scholar
  17. 17.
    Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: parallel analysis of alloy models by range partitioning. In: 2013 IEEE/ACM 28th International Conference on Automated Software Engineering (ASE), pp. 147–157. IEEE (2013)Google Scholar
  18. 18.
    Seater, R.M.: Core extraction and non-example generation: debugging and understanding logical models. Master’s thesis, Massachusetts Institute of Technology (2004)Google Scholar
  19. 19.
    Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 94–105. IEEE (2003)Google Scholar
  20. 20.
    Torlak, E., Chang, F.S.-H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 326–341. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-68237-0_23 CrossRefGoogle Scholar
  21. 21.
    Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71209-1_49 CrossRefGoogle Scholar
  22. 22.
    Winston, P.H.: Artificial Intelligence, 3rd edn, pp. 150–356. Addison-Wesley, Reading (1992)Google Scholar
  23. 23.
    Zayan, D., Antkiewicz, M., Czarnecki, K.: Effects of using examples on structural model comprehension: a controlled experiment. In: Proceedings of the 36th International Conference on Software Engineering, pp. 955–966. ACM (2014)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.Electrical & Computer EngineeringUniversity of WaterlooWaterlooCanada

Personalised recommendations