1. SCADE KCG工具能将基于Lustre的建模语言翻译到C语言，是不是能直接将Lustre语言翻译为C语言？

    在基于同步语言的开发工具中，最著名的是Scade，Scade是基于同步数据流语言Lustre的建模与开发工具，将一种扩展的Lustre语言翻译成C语言。

    SCADE KCG是一个代码生成器，确保输入模型符合语法语义，生成符合安全约束的C或Ada代码。

  2. SCADE开源吗？KCG开源吗？

    SCADE是一款商用编译器，非常昂贵，不能用来做二次开发。

  3. 什么是Clight？与C语言有什么关系？

    Clight是CompCert中使用的C语言的一个很大的子集。

  4. S2M工具用的单时钟还是多时钟？

    （在单时钟模型中，整个系统中的所有行为触发都由一个全局时钟所控制。其优点是对系统功能行为的描述更加简单，并且容易生成仿真代码。然而，在单时钟模型中，各个组件的时钟将与系统 全局时钟有严格的隶属关系，这将导致子系统的时钟间产生紧耦合，一旦一个组件的时钟频率出现变化，全局时钟以及其他组件的时钟也需要进行相应的调整。Lustre采用单时钟模型。

    与单时钟模型不同，多时钟模型没有全局时钟，各个组件都按照自己的时钟工作。组件之间是松耦合的，时间同步操作只需在进行交互的组件之间进行。因此，多时钟模型适合对分布式系统或具有高度并行性的系统进行建模，但是，多时钟会带来模型中信号间同步的复杂性，一方面，模型需要进行一致性的验证，另一方面，也增加了仿真代码生成的难度，signal采用多时钟模型。lustre同步数据流语言（一））

  5. L2C单时钟版本怎么使用？

    不用管了，用不上，稍微了解一下机制就行。

  6. S2M工具怎么和kind2连接起来？

    S2M工具前端基于Lustre的状态图模型，可以直接用kind2进行验证，了解一下验证相关模型需要的数据，以及怎么调用。

  7. 为什么后端用kind2验证的话要将Lustre语言转换成c语言？

    kind2验证是在Lustre转换之前，验证之后再进行C代码转换，以编写应用程序。

  8. S2M工具后端验证用的Z3工具吗？

    S2M 是在开源建模工具 Modelio 和开源验证工具 Z3 的基础上设计并实现的，支持 S2MSM 语言的建模和验证。

  9. S2M前端输入的是Lustre语言吗？

    前端输入的是模型，基于Lustre建模语言。

  10. Modelio是将状态机模型转换为Lustre语言吗？

    差不多这个意思？

  11. Z3和Kind2的异同与优缺点？

    • kind2用的是lustre语言进行验证，Z3我之前用的是c++。
    • 其它的还不知道。（我怎么感觉Z3简单一点？）