同步C哈特：基于状态的视觉同步模型的复杂瞬时行为和系统演化的微步骤

理论计算机科学电子札记88（2004）3-19www.elsevier.com/locate/entcs计算SyncCharts反应查尔斯和雷I3 S实验室（UMR 6070）尼斯大学Sophia Antipolis /CNRSSophia Antipolis，法国摘要SYNC C HARTS是一种基于状态的视觉同步模型。虽然使用简单的图形语法，同步C哈特可能会表现出复杂的瞬时行为，混合并发的演变，抢占和状态re-incarnations。本文解释了这样的反应中的微步骤。底层语义是一种构造性语义，与ESTEREL语义是在一个半正式的方式，从并发反应细胞的合作。1介绍反应系统是离散事件系统。它们大多是事件驱动的，这意味着它们很少自己进行处理，它们的行为可以表示为对刺激的一系列反应。描述连续演化的经典方法是求助于状态转换模型.然而，最简单的自动机形式并不方便应付现代应用的复杂性。表示这样的系统的层次结构意味着分层描述，支持并发和同步，以及系统的不同部分之间的通信。同步语言已经被引入来解决反应式系统编程的问题。在命令式同步语言ES-TEREL[1]中，通信和同步在信号的概念下统一起来。引起反应的刺激与排放有关1电子邮件：andre@unice.fr1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.05.0074C. André/Electronic Notes in Theoretical Computer Science 88（2004）3和信号的接收。信号也是抢占的参与者，使得暂停（冻结）或中止系统某些部分的行为成为同步模型采用了一个简化的假设：系统只在离散阶段（瞬时）演化，其持续时间为0。因此，反应的计算，这可能是由于程序的各部分之间的复杂相互作用，应该是瞬时的。这个强有力的假设，增强了信号的瞬时广播的假设，允许确定性的行为，即使在并发和抢占的存在ESTEREL擅长表达复杂的反应行为，但它不直接支持层次通信方面的规范有限状态机。SYNC CHARTS[2]已经作为图形化的Esterel语言的一种形式，将国家视为一等公民。作为Esterel的直接后代，SyncCharts继承了该语言的数学另一方面，SyncCharts的外观（语法）归功于Harel这种双重继承可能会误导初学者：syncChart2看起来像一个状态图，但它的行为可能不同。本文的第2和第3部分主要是教育性的。他们的目的是通过简单的例子来让读者对SyncCharts的语义有所了解。SyncCharts-一个明显简单的模型-可能有复杂的（瞬时）反应，严格遵守同步假设。这些反应反映了第4节中介绍的SyncCharts的底层语义。语义是用尊重构造性的因果关系：在进行测试之前，信号的存在状态必须是在前一个微步处终止。这就是G.贝里是埃斯泰尔语的意思。这种语义以半形式化的方式呈现，严重依赖于SyncCharts的结构。 这个结构是由UML模型精确定义的。一个更该模型及其语义的详细介绍，以适合于微步级仿真的操作风格给出，可在本文的扩展版本中获得[5]。2SyncCharts之旅2.1说明实例同步心脏由其结构的状态和转换以及其动力学的一个典型的同步图如图所示1.一、2S YNC C HARTS是模型。syncChart是模型的一个特定实例。C. André/Electronic Notes in Theoretical Computer Science 88（2004）35ABSync检测等待A和B1空闲WAWB臂复位A/臂B/臂定时器2 T /解除武CNT2dADB/ABInhib解除武装做信号臂信号解除Fig. 1.典型的SyncChart：这个SyncCharts指定了同步事件的检测器。信号AB必须在A和B以任何顺序发生时发出，但在时间上“足够接近”。 “Close enough” means that there are at most two occurrences ofA和B。复位是一个信号重新初始化信号。最后，抑制是一个信号，使2.2SYNC CHARTS的简化实现2.2.1结构一个状态可以是一个简单的状态，画成一个简单的圆形或椭圆形，也可以是一个画成圆角矩形的宏状态。一个宏观国家被定义为：它包含其他国家。一个简单的国家不会。一个状态可以有一个名字：写在内部的是简单状态，写在一个字符串中的是宏状态。转换是两个状态（从源状态和目标状态）之间的有向链接。有三种类型的过渡：强流产，弱流产和正常终止过渡。 从状态转换为到状态dA是一个强流产过渡。从状态Detection到自身的自循环转换，以及标记为Disarm的自循环转换是弱的中止转换。最后，从状态WaitAandB到状态done的转换是正常终止一个.状态转换图（STG）是一组连接的状态。STG必须有一个初始状态，用一个指向它的弧线表示。状态检测，wA，wB.是不同STG的初始状态。STG也可以有最终状态，用双圆圈表示。状态dA和dB是最终状态。STG必须包含在一个宏观国家中。当多个STG处于同一宏状态时，它们由虚线分隔，并且它们被称为并发的。 请注意，与statecharts相反，SYNC C尊重严格的遏制政策：没有级别间的过渡。宏状态检测包含两个并发的STG，宏状态WaitA和B也是如此。从状态传出的转换是有序的：一个称为优先级的整数被附加到转换的原点。例如，两个转换离开状态检测。强堕胎过渡具有优先级1，而弱堕胎过渡具有优先级2。6C. André/Electronic Notes in Theoretical Computer Science 88（2004）3堕胎过渡优先事项2。宏状态定时器底部的标签可以与过渡、初始弧或悬挂弧相关联。这些标签指的是下一小节中给出的信号。2.2.2信号.信号是我们处理通信和同步的独特抽象发射或接收信号符合事件的经典概念。信号具有存在状态：存在（+）、不存在（-）或未知（-）。可能传递给定类型的值。 如果一个信号可以在几分钟内发射几次，一个反应，还需要组合功能。不传递值的信号称为纯信号。 最后，信号有一个作用域：外部的 或宏观国家的地方。外部信号进一步分为输入信号和输出信号。本地信号是双向的，但仅用于内部通信。本地信号在syncChart上明确提到：arm是macrostateDetection的本地信号;disarm是macrostateABSync的本地信号。外部信号没有在syncChart中显式声明。最外面的宏状态的输入信号是A、B、复位、T和抑制。只有一个输出信号：AB。2.2.3与过渡相关联的标签。标签的一般语法是trigger [ guard ]/ e_select。 触发器可以是单个信号，其存在预期触发转变。可选的整数因子指示预期信号的若干连续出现（例如，宏状态定时器中转换的触发更复杂的触发器是使用逻辑运算符（and，or，not）的信号表达式。守卫是一个计算结果为true或false的表达式。 表达式使用信号和常量的值。一个结果是一组（即时的）动作。发出信号是一种可能的行动。触发器、防护装置和触发器是可选的。2.2.4与简单状态关联的标签。结果可以与简单状态相关联。对于纯SyncCharts（即，仅具有纯信号的syncChart），该事件由可能为空的一组发射信号组成。标签的语法为/e ect。C. André/Electronic Notes in Theoretical Computer Science 88（2004）372.3非形式语义学到目前为止，我们只介绍了SYNCCHARTS的语法方面。由于SYNCCHARTS旨在表示反应行为，因此主要的事情是理解模型的动态。在本节中，解释保持非正式。此外，我们专注于纯syncCharts，也就是说，syncCharts与纯信号。反应性与信号的存在/不存在有很强的联系纯同步心图足以解释一个反应的本质。这种简化的方法已经成功地用于ESTEREL2.3.1反应与其他同步模型一样，syncChart也是循环执行的。进化周期如下：(i) 读取输入：在我们的限制演示中，这意味着(ii) 计算反应：根据syncChart的内部状态和输入图像，计算新的内部状态和输出图像（即，为每个输出信号找到其新的存在状态）。(iii) 执行输出（即，有效地将输出信号传送到环境）。这个过程应该不需要时间。一个瞬间的特征完全在于相关的反应。注意，反应必须是确定性的。因此，以完全确定性的方式计算syncChart的反应是一个核心问题。2.3.2通信FSM。第一种方法是将syncChart视为一组通信有限状态机（syncChart中包含的每个STG的状态机）。 “有限状态机是由有限的一组存在条件（称为状态）和由事件触发的状态之间的同样有限的一组转换指定的机器。这个定义是由B。P.Douglass [6]适用于SYNC CHARTS，前提是事件被信号取代。像往常一样，一个状态表征了一种可能持续相当长一段时间的状况。当处于一种状态时，系统对一组信号作出反应，并可以根据它接受的信号到达（采取或触发转换）其他状态。假设状态wA、wB和空闲在syncChartABSync中是活动的。如果A存在，则进行从状态wA到状态dA的转换。执行相关的事件（本地信号臂的发射）。现在，这个信号8C. André/Electronic Notes in Theoretical Computer Science 88（2004）3广播.国家闲置等待武器的存在。 ARM的存在触发从空闲状态到宏状态定时器的转换。进入宏状态定时器，导致激活定时器中STG的初始状态。在这种反应中，进一步的进化不再可能。因此，在该反应期间不发射信号AB（存在状态设置为不存在）。 因此，在本发明中，反应表现为由因果关系驱动的一系列瞬时转变或微步骤。全局结果是激活状态的瞬时变化。因果链可能是循环的：它的瞬间执行显然是不可接受的。在这种情况下，syncChart被拒绝。前面的反应只意味着简单态上的强流产跃迁。强堕胎也适用于宏观国家。当复位存在时，无论其他输入信号的存在状态如何，宏状态检测都退出，而没有宏状态的任何先前内部演变。目标状态是相同的宏状态，检测在反应期间重新进入，并递归地激活封闭的STG的初始状态。 弱流产是不同的执行：在退出弱中止转换的宏状态起源之前，执行宏状态的内部演化（参见下面的示例）。正常终止转换没有显式触发器。 一旦源宏状态的每个STG处于最终状态，就触发这样的转换。例如，如果状态dA和wB是活动的，并且B存在，则采取从wB到dB的转变。现在，处于宏状态WaitA和B的两个STG处于最终状态。瞬时，进行正常终止转换，发出信号AB，并且状态done变为活动。我们现在可以说明这个例子中唯一的弱流产转变的触发。 假设状态dA、wB和cnt是活动的。 如果B和T都存在，并且T是自cnt激活以来第二次出现的T，则syncChart的反应是什么？采用触发器为“2 T“的转换发出本地解除信号。弱中止被触发，但在退出宏状态检测之前，必须执行可能的内部演化。这是前面给出的宏状态WaitA和B的正常终止的情况因此，发射信号AB。 现在，检测中不可能有进一步的进化;宏状态检测被有效地退出，然后重新进入，就像已经解释过的强流产一样。请注意，当从同一状态发出的几个转换同时符合触发条件时，只采用具有最高优先级（最小整数值）的转换。为了避免不一致的决定，SYNC CHARTS施加了以下限制：强流产优先于弱流产，弱流产优先于正常终止。正常的终止不是严格必要的：同样的行为可以C. André/Electronic Notes in Theoretical Computer Science 88（2004）39dAdB/AB做信号臂dA/DAdB/DBDA和DB /AB做信号臂，DA，DB通过由本地信号的结合触发的弱流产获得（见图1）。2）的情况。我们保留了这个比弱堕胎对应物更具可读性的方便构造。图二. 正常终止可被弱流产和局部信号所取代。最后，暂停被用来“冻结”宏观国家内部的演变。当抑制存在时，定时器将忽略可能出现的T，当然，也不能发射解除武装。这几个例子显示了反应的复杂性，这可能是由于部分有序的过渡放电。事实上，通信FSM并不能很好地适应层次结构、抢占，尤其是转换触发的瞬时链接。而不是通信FSM，我们选择合作的反应细胞作为主动代理。2.3.3反应细胞。在SYNCCHARTS中，默认行为是永远保持一种状态。 一个状态只能通过触发一个流产过渡（回想一下，正常终止是弱流产的一个特例），或者通过退出一个包含的宏状态来间接退出。因此，syncChart中的活动代理是具有其传出转换的状态。我们称反应细胞为一种具有传出跃迁的状态一反应性单元可以是活动的（存活的）或空闲的（根本不做任何事情）。 一个积极的重新-活动单元永久地测试与其转换相关联的触发。一旦可以进行转换，则去激活反应单元，并且激活转换的反应单元目标。 现在的反应是激活/去激活在细胞集合中的传播。这种执行模型受到Boussinot的反应式对象的启发反应细胞将用于我们更正式的模型演示（第二节）。4）.10C. André/Electronic Notes in Theoretical Computer Science 88（2004）3过渡t新状态发射信号B−→#b−−→#b◦−−→{q}{r}{r}b，Bb，B，C和218cpa/BQR不/A/B/C图三.即时反应：当p处于活动状态且a发生时，根据应用于状态q的抢占类型的行为。3高级功能3.1立即抢占当在宏状态WaitA和B中进入状态wA时，如果此时A存在，则不进行输出转换。这是通常的行为：触发器等待严格的未来事件。这种默认行为可以使用转换的立即限定符（由触发器前面的#符号表示）进行修改。通过立即转换，一些状态可以可能变成瞬时的，也就是说，在相同的反应过程中被激活然后失活。请注意，它们仍然是真正的状态，因为在某些情况下，控制可以留在其中。即时反应与抢占相结合会导致不同的行为，如图所示。3 .第三章。 注意，在这个例子中，立即强中止使得状态q被绕过。3.2重新化身循环、立即抢占和优先级可以导致惊人的、但完全一致的行为。图图4显示了一个特别设计的例子来说明这些复杂的相互作用。在这个例子中，我们使用有值信号来获得更好的可追溯性，但微步的连续性与纯信号相同。信号v是具有作为组合函数的乘法的整数。每个跃迁发射的值都是不同的素数，因此，v传递的值忠实地反映了反应3中发射的跃迁。假设状态S1是活动的。如果信号a、b、c和d存在，则v存在，其值为11550= 2<$3< $52< $7< $11。新的活动状态是s3。该反应可以非正式地分解如下：(i) MacrostateinnerMacro必须被标记为c，其具有高于由d标记的优先级。3组合函数不能保持顺序，组合函数必须是可交换的！C. André/Electronic Notes in Theoretical Computer Science 88（2004）311轮回信号v：=1：将整数与 * innerMacro组合/v[2]1S12# b /v[5]a /v[3]S212# d /v[11][7]第七章S3见图4。 国家轮回。(ii) 在触发转换之前，必须执行宏状态的内部在内部，它是由a触发的强流产，被采取，发射v（3）。(iii) 状态s1是目标，因此重新输入s1。事实上，这是s1的一个新实例（re-incarnation）。(iv) 这个新的事例可以接受a的严格的将来发生，也可以接受b的现在或将来发生。因此，采用由b触发的跃迁，并且用5发射v状态S2被激活。(v) 由于状态s2没有传出跃迁，因此在innerMacro中不可能有更多的演化。然后，由c触发的转换被触发。V以值7发射。(vi) 转换的目标是重新输入的macrostateinnerMacro再次，这是一个轮回。这个新的实例可以接受c的严格的未来出现，也可以接受d的现在或未来出现。d触发的弱流产然后被采取，但在此之前，innerMacro内部必须做出反应。(vii) innerMacro的执行开始于发出值为2的v（初始弧）并进入状态s1。(viii) s1的这个新实例可以接受a的严格未来出现，也可以接受b的现在或未来出现。因此，采用由b触发的跃迁，并且用5发射v状态S2被激活。(ix) 由于状态s2没有传出跃迁，因此在innerMacro中不可能有更多的演化。然后，由d触发的转换被触发。v的值为11。(x) 状态s3被激活，并且反应停止。因此，v表示值3< $5< $7<$2<$5< $11。概括地说，这是一种完全可以解释的行为，几乎是显而易见的。12C. André/Electronic Notes in Theoretical Computer Science 88（2004）3+watrans0.. *+satrans0 ..*+内流+退出+effect0..10.. 1+悬浮液{ordered}{ordered}0..10..10.. 10..10+nttran0.. 1+rcells1. *+顶部10..1+起始+stgs11. *STG初始弧宏观状态NormalTerm反应电池可疑弧+isFinal：booleanSimpleStateInstantActionStrongAbortWeakAbortSyncChart4SyncCharts的正式介绍同步图表基于状态和时刻。通常，基于实例的模型的语义被给出为可能的刺激/反应序列对（输入序列/输出序列）的集合。 该集合由下式隐式给出： 接受程序或归纳建构机制。在本文中，我们选择后者。因此，我们需要一个syncChart结 构的 正式 定 义（ 第二 节 ）。 4.1 ） 。然 后， 我们 必 须描 述syncChart的状态和它的环境。 为此，上下文定义（Sec. 4.2）。最后，我们必须给出一个语义：在SEC中。4.3，我们引入了操作构造语义。.. 1+身体状态1图五. SYNCCHARTS4.1元模型SYNCCHARTS的抽象语法是使用标准UML符号表示的。图5涵盖了与状态相关的基本概念。一个ReactiveCell由一个body和可能为空的outgoing transitions集合组成。主体是一个状态：Macrostate或SimpleState。satrans是强终止转换的集合;watrans是弱终止转换的集合;nttran是最多包含一个转换的正常终止转换的集合。格式良好的SyncChart还必须遵守一些约束：• STG必须是连通图。• 一个Transition连接同一个STG中的两个反应单元。• 一个最终的简单状态，既没有向外的转移，也没有相关的效应。syncChart的结构可以由反映状态包含层次结构的树表示。更准确地说，一个宏状态包含STG，一个STG包含反应单元，一个反应单元包含一个且仅一个状态。在树中，ReactiveCell有且只有一个后继。可以省略C. André/Electronic Notes in Theoretical Computer Science 88（2004）313而不丢失关于结构的信息。生成的树有两种类型的节点（state和STG），它们在树的任何路径上交替。图6给出了我们的符号和与ABSync相关的树。请注意，代表状态的实心圆有三种变体：无悬浮的宏观状态、悬浮的宏观状态和简单状态。ABSync检测等待A和B定时器做空闲瓦达wB dBCNT见图6。 与syncChart关联的树。4.2配置和信号上下文4.2.1配置。Harel和Naamad [8]将配置定义为可以同时激活的状态的最大集合。必须对该定义进行调整，以考虑暂停情况。设T为与syncChart相关联的顶部宏状态。用于T的配置C（因此，用于syncChart）必须满足以下规则：(i) T在C中。(ii) 如果一个没有悬浮的宏观状态M在C中，那么对于每个STG，C也必须包含直接包含在M中的G，恰好一个直接包含在G中的状态。(iii) 如果具有悬浮M的宏观状态在C中，则• C不能包含M的状态后代• 或者，对于每个STG，C也必须包含直接包含在M中的G，恰好一个直接包含在G中的状态。(iv) C只包含满足规则1到3的状态。可以从与syncChart关联的树中导出配置标识符标识符无悬浮液的具有悬浮状态的宏状态简单状态STG传奇14C. André/Electronic Notes in Theoretical Computer Science 88（2004）3这棵树必须被认为是一棵AND/OR树，其中AND节点是实心圆（状态），OR节点是空心圆（STG）。{ABSync，Detector，WaitAandB，wA，wB，idle}、{ABSync，Detector，WaitAandB，wA，wB，Timer}和{ABSync，Detector，WaitAandB，wA，wB，Timer，cnt}是syncChartABSync的配置实例。4.2.2信号上下文。由于SYNCCHARTS中的反应可能是由几个子系统的瞬时合作引起的，因此支持通信的信号是SYNCCHARTS语义中的每个反应都与一组称为信号背景的信号E相关联。E被划分为两个块：E+和E-（即，E=E+E−和E+E−=4. E+是当前时刻的当前信号的集合，E-是当前时刻的当前信号的集合。缺席的信号。 在一个瞬间，信号必须存在，无托叶在计算反应时，只有由环境施加的输入信号才具有确定的状态。必须确定所有其他信号的存在状态。 像在ESTEREL语言中一样，我们假设非输入信号存在，当且仅当它在瞬间发出4.3建构语义学导论问题4.1给定一个纯syncChart，它的一个配置，以及所有输入信号的存在状态，计算反应，（即，下一个配置和所有输出信号的存在状态）。4.3.1反应的计算原理我们认为syncChart作为一个相互作用的反应细胞的集合。每个细胞都接收触发进化的信号，这些信号可能会发出新的信号。所有的信号都是即时传播的。从概念上讲，反应单元同时运行。每个活动的反应性单元局部地确定其行为（即，执行动作、进行转换并因此变为空闲或保持活动）。信号的存在状态是决定信息。为了确保syncChart反应的确定性，所有反应单元必须就每个信号的实际存在状态达成一致。这假设通过对话找到一个定点解决方案。为了解决这个问题，我们建议每个反应细胞暂停其evolution时，在怀疑的触发信号表达式的值。相应的评价尚待进行。当一个仍在运行的并发单元4在ESTEREL中，当前输入信号的集合称为输入事件。我们避免使用这个术语，它通常与单个信号的出现有关。C. André/Electronic Notes in Theoretical Computer Science 88（2004）315发射信号时，关于所发射信号的存在状态的这一事实被广播到其它小区。该可靠的新鲜信息可以断言或反驳未决的评估，并且因此恢复小区的演进。 该过程被应用直到稳定，当每个活动单元已经终止其演进或被暂停时。在后一种情况下所做的取决于所选择的语义。下面将描述一些语义变体。然而，我们必须精确地定义信号表达的解释。注4.2这种方法类似于G. Berry [4]为ESTEREL语言。他将其命名为构造性语义学，因为值是通过显式证明计算的，而不是通过错误4.3.2信号代数当反应已经被成功计算时，存在和不存在信号中的信号上下文然而，在com-假设本身，信号的存在状态可能是未知的。现在，E+是在当前时刻确定存在的信号的集合，E-是确定不存在的信号的集合，并且E是信号的集合，其状态是还不知道。不处理布尔值，我们求助于斯科特布尔域B<$={<$，−，+}，其中<$<+和<$<−。用于确定上下文E的技术是传播事实并逐步构建解决方案（如果存在的话）。计算依赖于单调函数。顺序关系定义为：E≤EJE+EJ+E−EJ−信号被组合在例如触发器中使用的信号表达式中。 信号表达式是类似于布尔表达式的表达式，由信号、运算符（not、or、and）和括号组成。给定信号上下文E，信号表达式Φ在B中求值：对于Φ：：=σ（对于信号 σ）|不是φ|φ或φ|φ和φ。 φ被计算为如下所示：eval（σ，E）=+ ifσ∈E+，− ifσ∈E−，否则eval（notφ，E）=not eval（φ，E）eval（φorφ，E）= eval（φ，E）oreval（φ，E）其中，运算符not、or、and和在下表中定义。16C. André/Electronic Notes in Theoretical Computer Science 88（2004）3不⊥⊥-++-或⊥-+⊥⊥⊥+-⊥-+++++和⊥-+⊥⊥-⊥----+⊥-+4.3.3反应性细胞的反应。反应性电池的反应依赖于其组分的反应。react（）方法是为不同的类定义的。此方法返回一个终止状态，该状态采用枚举{DONE，DEAD，PAUSE}中的值。返回DONE意味着对象已经终止了它的反应，并且在下一个瞬间没有任何事情要做。返回PAUSE意味着它的反应在当前时刻结束，但将在下一时刻继续。最后，DEAD意味着对象已经终止了它的反应，除了等待正常的终止之外，在下一个瞬间没有什么可一旦进入最终状态，react（）返回DEAD，直到有效的正常终止。react（）方法的伪代码和注释在本文的扩展版本中给出[5]。请注意，我们的目标不是高效地编译SyncCharts，而只是解释微步骤。我们的解决方案严重依赖于并发执行，而大多数编译（共E STEREL程序）试图串行化并发演进（例如， 见S.Edwards4.3.4一个潜在的功能。如果递归计算返回，则syncChart现在处于新的配置中，并且在反应期间使用的所有信号都被赋予了明确的存在状态。默认情况下，所有其他信号都设置为不存在。反应的计算是成功的。然而，计算可能会停止与暂停反应细胞。对于ESTEREL程序和反应对象，F. Boussinot [11] 研 究 了 不 同 的 方 法 来 恢 复 计 算 。 这 些 想 法 也 适 用 于SYNCCHARTS。在reactive对象中使用的更激进的解决方案是设置为不存在所有尚未分配的信号，恢复挂起表达式的求值，并将决策的发布推迟到下一刻SYNC C HARTS，像E STEREL一样不会推迟决定。相反地，他们试图丰富他们关于信号背景的知识。最有趣的信息是关于在反应期间肯定不存在（不能发射）的信号。要知道一个信号是否不应该被发射，似乎与千里眼有关。事实上，使用结构（语法分析），我们构建了一个单调递减的潜在发射信号集，称为C. André/Electronic Notes in Theoretical Computer Science 88（2004）317潜力如果该集合是正确的（即，所有可能发射的信号都在电势中）。考虑到电势，停滞的反应可以恢复，以微步进行，然后再次停滞。重复该过程，并且最终，该过程在所有存在状态被定义的情况下停止，或者仍然存在暂停的评估并且电位不能帮助待决的评估。在第一种情况下，反应成功完成。在后一种情况下，syncChart被拒绝为非建设性的。势函数的选择至关重要。一个粗糙的势很容易计算，但会导致许多不合理的syncCharts拒绝;一个精细的势很难构造，但接受一个大类的SYNCCHARTS。在Esterel Studio中使用的SYNC CHARTS的商业版本[12]将syncChart翻译成等效的Esterel程序，然后编译。因此，势函数是在Esterel V5编译器中使用的函数，基于利用syncCharts结构的有效势函数的研究仍在进行中。5结论和展望这篇论文表明，同步C哈茨可以隐藏复杂行为。实际上，SYNCCHARTS是图形对应物ESTEREL，一种文本语言。 任何syncChart都可以转换为等 价 的 ESTEREL 程 序 ， 这 是 编 译 SYNC- CHARTS 的 常 用 方 法 。 对 于 熟 悉ESTEREL语义的人来说，SYNC CHARTS的行为很容易理解。例如，令人惊讶的状态再化身示例可以被视为ESTEREL信号再化身的简单图形变体与其利用这种密切的关系，同步CHARTS和在此基础上，我们选择将SYNCCHARTS作为一个独立的基于状态的同步模型.SYNCCHARTS的结构已经通过元模型使用UML符号正式定义。反作用的计算已经用协同反应单元来解释了.构造性语义学的原理也得到了解释，但没有形式化5。我们相信，对于许多更熟悉状态图模型而不是编程语言的工程师来说，像SYNCCHARTS但同为与ESTEREL语言一样具有表达力，SYNC CHARTS可能过于强大-对于转世的例子就是一个很好的例子。5有一个关于SYNCCHAR ts的行为语义的技术报告[13]（早期版本）。18C. André/Electronic Notes in Theoretical Computer Science 88（2004）3此外，即使是高级用户，也可能仅使用SYNCCHARTS可能性我们计划开发一个专用于同步CHARTS的平台，• 为了选择他/她想要使用的构造集合（定制），• 为了跟踪微步执行（理解语义），• 反应（模拟）。因此，用户可以使他/她的模型适应他/她的需求。当然，更简单的模型更容易学习，并且可能导致更有效的编译。 例如，即时修饰符是非常有趣的即时-这是一个新的对话，但它可能很容易引入因果循环。 丢弃im-mediate使第一个即时反应简单得多：在刚进入的状态上，既不会发生强流产，也不会发生弱流产。其他可能性涉及潜在函数的选择。甚至可以引入信号处理的变化：在某些情况下，例如为了消除因果循环，可以方便地将某些信号的发射延迟到下一时刻，如在Statecharts中所做的那样。所有这些变化都很容易形成和实施。元模型中添加了额外的约束至于语义，修改react（）方法就足够了。引用[1] G.贝瑞埃斯特雷尔的基础。In C.斯特灵湾Plotkin和M. Tofte，编辑，证明，语言和互动：纪念罗宾米尔纳的论文。麻省理工学院出版社，2000年。[2] C. 还有。 R epr ent a t iona在系统应用计算工程（CESA），第19IEEE-SMC。[3] D. 哈雷尔S TATECHARTS：A visual formalism for complex systems. 计算机科学Programming，8：231[4] G. 贝瑞纯埃斯泰尔的建构语义学。（1999年修订版），可在网上查阅，www.esterel-technologies.com网站， Sophia Antipolis（女），1999年7月。[5] 查里莱和里莱。计算系统是一个简单的系统。TechnicalReportISRNI3S/RR-2003-09-FR，I3S，Sophia-Antipolis，France，April 2003.[6] B. P·道格拉斯实时设计模式。对象技术系列。Addison-Wesley，Reading，Massachusetts，2003.[7] F.布西诺湾Doumenc和J-B.史蒂芬妮反应对象。Ann. Telecommunication，51（9[8] D. Harel和A.娜玛德statecharts的STATEMATE语义。ACM Trans. Soft.工程方法。，5（4）：477[9] Stephen A.爱德华兹一个用于大型控制系统的esterel编译器。 IEEE Trans. on Computer-AidedDesign of Integrated Circuits and Systems，21（2）：169C. André/Electronic Notes in Theoretical Computer Science 88（2004）319[10] E. Czech，M. Poize，J. Pulou，P. Venier，and D. 好吧S轴-RT： 解读ESTEREL语义上的顺序执行结构。在理论计算机科学中的电子笔记，第65卷（5），格勒诺布尔（F），2002年。Slap[11] F. 布西诺Sugarcubes实现 因果关系。Technical Report 3487，INRIA，September 1998.[12] Esterel Technologies，Guyancourt（女），//www.esterel-technologies.com. EsterelStudio，V4，2002. 参考手册。[13] 我是查理。 系统特征：一个虚拟化的过程代表了一个虚拟化的过程。TechnicalReportRR 95RR（96-1996年4