ILAng
  • Introduction
  • Getting Started
    • Installing ILAng
    • ILAng with CMake
    • ILAng with Python
    • ILAng in Docker
  • Modeling
    • ILA Model
    • Architectural States
      • Expressions
      • Uninterpreted function
    • Instructions
    • Hierarchical ILA
    • Conclusion
  • Synthesis
    • Writing Templates
    • Interfacing Simulators
    • Synthesis Results
    • Conclusion
  • Verification
    • Refinement Relation
    • Verification Target
    • Examples
    • Notes
  • Development
    • Release Notes
Powered by GitBook
On this page
  • Export the synthesis result
  • Import the synthesis result
  • Synthesis result in ILAng

Was this helpful?

  1. Synthesis

Synthesis Results

Once the synthesis process finishes successfully, all partially defined AST expressions (synthesis primitives) will be replaced by a concrete normal AST expression.

Export the synthesis result

The synthesis result can be exported and archived into a machine-readable format. To export the whole model:

m.exportAll('file_name.txt')

To export only the state update function of one single state:

m.exportOne(m.get_next('state_var_name'), 'file_name.txt')

When exported, the state update function (expression) is the conjunction of the state update functions under all provided instructions.

Import the synthesis result

To import the whole model from a file:

m = ila.Abstraction('placholder_name')
m.importAll('file_name.txt')

You can also import a single state update function (or any expression):

some_expression = m.importOne('file_name.txt')

Synthesis result in ILAng

To utilize the synthesis result (from Python environment) in your C++ project using ILAng, an ILA model can be automatically constructed from the exported result:

#include <ilang/synth-interface/synth_engine_interface.h>
auto m = ilang::ImportSynthAbsFromFile("result.txt", "ila_name");
PreviousInterfacing SimulatorsNextConclusion

Last updated 6 years ago

Was this helpful?