Return to search

En optimierande kompilator för SMV till CLP(B) / An optimising SMV to CLP(B) compiler

<p>This thesis describes an optimising compiler for translating from SMV to CLP(B). The optimisation is aimed at reducing the number of required variables in order to decrease the size of the resulting BDDs. Also a partitioning of the transition relation is performed. The compiler uses an internal representation of a FSM that is built up from the SMV description. A number of rewrite steps are performed on the problem description such as encoding to a Boolean domain and performing the optimisations. </p><p>The variable reduction heuristic is based on finding sub-circuits that are suitable for reduction and a state space search is performed on those groups. An evaluation of the results shows that in some cases the compiler is able to greatly reduce the size of the resulting BDDs.</p>

Identiferoai:union.ndltd.org:UPSALLA/oai:DiVA.org:liu-2805
Date January 2005
CreatorsAsplund, Mikael
PublisherLinköping University, Department of Computer and Information Science, Institutionen för datavetenskap
Source SetsDiVA Archive at Upsalla University
LanguageSwedish
Detected LanguageEnglish
TypeStudent thesis, text

Page generated in 0.0018 seconds