Herramientas Personales
Usted está aquí: Inicio → Investigación → Grupos de Investigación → rfm → Alloy_HotCore
 

Alloy_HotCore

Description

Identifying a minimal unsatisfiable core in an Alloy model proved to be a very useful feature in many scenarios. Alloy+HotCore extends this concept to hot core, an approximation to unsat core that enables the user to obtain valuable feedback when the Alloy’s sat-solving process is abruptly interrupted.

Example

Please download the following example in order to test Alloy_Hotcore

Download

alloy_hotcore.jar Alloy 4.1.10 extended with the HotCore highlighting feature

About us

Alloy_HotCore was developed by the Relational Formal Group at the University of Buenos Aires, with the Collaboration of:

  • Esteban Lanzarotti Departamento de Computación - Universidad de Buenos Aires (estiben AT gmail DOT com)
  • Sergio Mera Departamento de Computación - Universidad de Buenos Aires (s LASTNAME AT dc DOT uba DOT ar)
  • D'Ippolito Nicolas - Universidad de Buenos Aires (ndippolito AT dc DOT uba DOT ar)

Bug report

Please send us any bug report to jgaleotti AT dc DOT uba DOT ar

Acciones de Documento