Motor simbólico: monolítico y composicional
Motor simbólico: monolítico y composicional
Este branch agrega dos nuevos motores de síntesis de controladores GR(1) basados en BDDs:
Motor simbólico monolítico (symbolic ||Controller): computa el punto fijo de mayor punto fijo de menor punto fijo (GR(1)) sobre la representación BDD de la composición paralela completa de la planta.
Motor simbólico composicional (symbolicCompositional ||Controller): divide el problema en sub-plantas, resuelve cada batch en forma incremental y acelera el punto fijo usando equivalencia fuerte (SSOE) para abstraer componentes ya procesados. El cálculo simbólico de WSOE usa composición relacional (relprod) sobre variables reservadas globalmente por SymbolicManager.
Ambos motores se activan desde FSP con la keyword symbolicCompositional (o symbolic para el monolítico), y se incluyen tests de integración para los casos realizables e irrealizables.