Home

Welcome to the VIATRA Solver, an efficient graph solver for generating well-formed models!

About

VIATRA Solver is a framework for automatically generating well-formed instance models for domain-specific languages.

• The framework natively supports instance generation for EMF metamodels, optionally, by extending an existing model. The generated models are presented as standard instances of the target domain.
• The solver creates models that satisfy well-formedness constraints of the target language, which is given as an input to the framework. Currently, well-formedness constraints can be specified in the VQL graph query language of the VIATRA query and transformation framework, but the solver framework is designed in a way to incorporate OCL constraints in the future.
• The framework translates the language specification to a logic problem, which is solved by an underlying first order logic solver to create valid graph models. Currently, our solution supports Alloy (with back-end SAT solvers like Sat4j and Minisat), Z3 SMT solver, and features a new graph solver. The framework use the background solvers automatically, so no additional skill is required by the language developers.
• The framework features a new graph-based logic solver that is able to generate valid models with more than 5000 objects. Additionally, our measurements shows that models generated by this graph solver are both more diverse and more realistic than the ones generated by other solvers (like Alloy).
• The framework supports the visualisation of output graph models and collects the runtime statistics of the solvers.
• The framework features an editor to select the target domain and to configure the generation process.

User Guide

Developer Guide

Publications

Reference:

@inproceedings {ViatraSolver,
	author = {Oszk{\'a}r Semer{\'a}th and Andr{\'a}s Szabolcs Nagy and D{\'a}niel Varr{\'o}}
	title = {A Graph Solver for the Automated Generation of Consistent Domain-Specific Models},
	booktitle = {40th International Conference on Software Engineering (ICSE 2018)},
	year = {2018},
	month = {5},
	publisher = {ACM},
	organization = {ACM},
	address = {Gothenburg, Sweden},
}