基于重写逻辑的交互混合系统形式化分析和自适应步长数值方法MuhammadFadlisyah等

理论计算机科学电子笔记274（2011）17-32www.elsevier.com/locate/entcs基于重写逻辑的交互混合系统形式化分析中的自适应步长数值方法MuhammadFadlisyahPeterCsabaOülveczky挪威奥斯陆大学信息学系ErikaA'brah'am德国亚琛工业大学计算机科学系摘要本文的重点是形式化的建模，仿真和分析的相互作用的混合系统，在彼此的连续行为。 我们定义了基于重写逻辑的实时Maude工具一种用常微分方程描述的连续动力学的数值近似方法。我们采用Runge-Kutta-Fehlberg4/5方法来定义一种自适应步长技术，该技术允许比固定步长技术更精确的近似，计算量更少。 我们 并给出了两个不同误差容限的热系统的实验结果关键词：形式化建模，交互物理系统，仿真，形式化分析，重写逻辑，龙格-库塔-费尔伯格方法1介绍Real-Time Maude[15]是一个高性能工具，它扩展了基于重写逻辑的Maude系统[4]，以支持基于对象的实时系统的形式化建模，仿真和分析。Real-Time Maude强调规格的易用性和表达性，并已被证明可用于分析广泛的超越时间自动机范围的高级应用，例如通信协议[16，13]，无线传感器网络算法[11，17]和需要无界数据结构的调度算法[14]。本文是研究如何使用Real-TimeMaude正式建模、仿真和分析混合系统的一部分，这项工作得到了挪威研究委员会通过Rhythm项目和DAAD ppp项目HySmart的部分支持。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.07.00418M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17连续的行为。特别是，我们考虑相互作用的物理实体，其连续的行为可以描述普通微分方程（ODE）。物理实体相互作用，并可能影响彼此的连续行为。例如，房间里的一杯热咖啡通过不同类型的热传递与房间相互作用我们的目标是开发一种技术，以产生可执行的模型，这样的系统在实时Maude。对于常微分方程描述的物理系统的连续行为，在我们以前的工作[7]中，执行是基于固定步长的数值方法，给出普通微分方程的近似解。也就是说，为了近似一个系统在我们使用欧拉和龙格-库塔二阶和四阶方法的小步骤近似。本文描述了自适应步长数值方法的积分，其中小时间步长的持续时间是动态选择的。自适应步长近似具有以下优点：（i）当需要接近必须进行离散转换的时刻或需要保持所需近似精度时，通过减小时间步长使分析更精确;（ii）当近似允许时，通过增加步长使分析更有效。特别是，自适应步长使用户能够定义自己的误差容限，以在所需精度和计算效率之间进行平衡我们开发了Runge-Kutta-Fehlberg 4/5方法的适应性（参见例如，[8]），这使我们能够根据用户提供的误差容限，用动态步长来我们描述了自适应方法在Real-Time Maude中的实现。此外，我们比较的结果和执行时间的模拟和模型检查使用不同的误差容限的两个热系统与现实的参数。混杂系统的数值仿真工具有多种。MATLAB/Simulink [20]提供了广泛的数值模拟方法。HyVisual [12]考虑了线性多步和Runge-Kutta方法。CHARON[6]还使用具有自适应步长的线性多步方法。 与这些工具相比，我们的方法除了支持建模和仿真外，还支持混合系统的形式化分析，如时序逻辑模型检测。我们的方法也不同于混合系统的模型检查器，如CheckMate [3]，PHAVer [9]，d/dt [5]和HYPERTECH [10]，因为我们不使用抽象或过度近似，但仍然支持建模，可达性分析和混合系统的全类LTL模型检查，通过（可能是非线性）ODE描述连续动态。 而其他正式的工具使用混合自动机，图表或块模型，或建模公式，我们使用重写逻辑作为底层建模形式主义。我们的方法的模型是复合的-其中，组件的连续动态可能取决于与其他组件的显式建模的交互。由于逻辑还支持类和对象以及任何可计算数据类型的定义，因此物理系统M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）1719∪通过一些程序控制，可以直观地建模和分析。本文的结构如下：第2节给出了一个概述的实时Maude。第3节简要介绍了我们的方法建模重写逻辑的混合系统。第4节介绍了龙格-库塔-Fehlberg 4/5方法的适应性，第5节描述了它在实时Maude中的实现。第6节总结了案例研究，第7节给出了结论性意见。2实时Maude一实时Maude定时 模块规格一实时 重写理论（R，E，IR， TR），其中：• （E，E）是一个隶属方程逻辑[4]理论，其签名为1，E一组连续和终止的条件方程。（E，E）将状态空间指定为代数数据类型，并包含对时域建模的排序时间的• IR是一组（可能是有条件的）标记的瞬时重写规则，其指定系统零时间）单步转换。这些规则被应用于对方程E取模。2• TR是一组（可能是有条件的）报价重写规则，它对时间流逝进行建模，用语法rl [l]：{t}=>{t′}（时间τ）crl [l]：{t} => {t′}（时间τ），如果条件其中τ是表示重写持续时间的排序时间项一个系统的全局状态是{t}形式的项;滴答规则的形式确保了时间在系统中均匀地前进。实时Maude语法相当直观（参见[4]）。例如，一个函数f的参数排序为s1. sn，sorts的值被声明为opf：s1.sn->s。方程写为eqt=tJ，如果条件方程为cond，则写为ceqt=tJ 变量用关键字var和vars声明。类声明类C|att1：s1，.，attn：sn. 声明一个类C，它的属性att1到attn的排序为s1到sn。 子类继承了它的超类的所有属性和规则。类C的对象表示为项 of sortObject，其中O，of sort Oid，是对象的标识符，val 1到val n是属性att 1到att n的当前值。 在并发面向对象系统中，状态是一种配置类型的术语。它具有由对象和可能的消息组成的多集结构。配置的多集并集由并置运算符（空语法）表示，并置运算符被声明为关联和可交换的，因此重写是实时Maude直接支持的多集重写。1即，排序、子排序和函数符号的声明2E是一个并集E′A，其中A是一组等式公理（结合性、交换性、恒等式等）。以A为模进行演绎。在应用任何重写规则之前，项被简化为它的E′-范式模A20M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17努力物理实体连续动力学属性流物理相互作用连续动力学属性图1.一、简单热系统中的物理系统组件及其相互作用Real-Time Maude规范在合理的条件下是可执行的，并且该工具支持各种形式化分析方法。重写命令（时间上的trewt< =τ.）模拟系统在持续时间τ内的一个公平行为，其中t是初始状态，τ是排序时间项。搜索命令使用广度优先搜索来分析系统的所有可能行为，并检查是否可以从初始状态到达与模式匹配的状态，从而满足给定条件。Real-Time Maude还扩展了Maude最后，find earliest命令确定达到所需状态所需的最短时间3建模物理系统在[7]中，我们提出了一个基于e-排序和e-流方法[21]的物理系统建模和分析框架。我们的工作和大多数其他形式的方法之间的一个关键的区别是，而不是考虑一个组件的连续行为孤立的混合系统，我们认为混合系统由一组物理组件，其中一个组件的连续动态可能取决于其他组件的连续动态。因此，物理实体之间的物理交互被视为一等公民，物理系统被建模为物理实体和物理交互的网络，如图1所示。一个物理实体由一组属性、一个实值变量和一个连续动力学组成。属性值只能由离散事件更改。例如，材料的相（固体、液体、气体、等离子体）经由离散相变而改变。e_t变量表示随时间演化的物理量，例如温度。它的连续动力学被表示为一个常微分方程（ODE）.物理实体可以具有与一个或多个物理实体的一个或多个物理交互。物理交互表示两个物理实体之间的交互。它由一组属性、一个实值的随机变量和一个连续动态组成。Wavelow变量表示通过杯的传导咖啡房间表面对流固体熔化液体蒸发连续行为离散行为M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）1721描述两个实体之间相互作用的量，例如，在热相互作用中的热流率。它的值由方程形式的连续动力学决定。一个物理实体的连续动力学是一个常微分方程，左边是它的时间导数，右边是一个可能涉及实体属性和连接相互作用的时间导数的表达式双重地，物理相互作用的连续动力学是一个方程，左手边是一个变量，右手边是一个表达式，可能涉及相互作用的局部属性和连接实体的这样可以避免物理实体的ODE的直接耦合[2]图1示出了表示房间中的一杯咖啡的热系统在热系统中，一个物理实体是一个热实体，它的等效变量（T）定义了实体的温度，它的连续动力学定义了随着时间的推移和温度的变化，实体获得或损失的同样地，物理相互作用是一种热相互作用，其热变系数（Qstec）表示加热流速。热相互作用的例子是传导、对流和辐射。它们的连续动力学由传热速率方程给出。物理系统组件的基本行为是它们的连续行为。我们使用单步，初值问题数值方法[2]通过在小的离散时间步长中推进时间来近似物理系统组件的在以前的工作中，我们已经集成了欧拉，龙格-库塔二阶，龙格-库塔四阶方法，我们的建模技术。然而，在这些方法中，执行中的小时间步长的大小是恒定的。4自适应步长数值方法为了近似一些具有快速变化或突变的连续行为，对于固定步长方法，我们必须选择较小的步长以获得满意的结果。然而，小的步长带来非常高的计算成本。例如，用我们的龙格-库塔四阶方法实现1000个时间单位，用步长1近似计算图1中的可压缩系统需要38分钟，但用步长0需要285分钟。5. 对于动力学更稳定的系统自适应步长技术的思想是通过估计和控制每一步的误差来适应逼近的轨迹这样的误差估计被用作动态地增加或减小步长的基础4.1逼近误差假设连续变量y具有时间导数YJ（t）=f（t，y（t））和初始值y（0）=y0。为了对某些T > 0近似y（T），小步长数值方法计算一系列值y1，y2，.，yN近似于22M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17n+1个n+1个nn+1个n+1个n+1个局部解局部误差局部误差.局部解全局误差全局误差.局部误差局部误差.全局误差全局误差.精确解图二、数值逼近中的局部误差和整体值y（t1），y（t2），.，y（tN）对于一些时间点t1p法4.p阶方法的局部误差可以通过比较结果是εl<$$ >n+1=y<$n+1−yn+1。可以证明这是正确的当h→0时的渐近结果 [19]。如果本地错误通过测试，则接受此错误，并在下一步中增加步长。对于每步误差条件，我们定义hn+1=α·hn如果不通过测试，则拒绝该步长并将其减小。对于每步误差条件，我们定义hJn=α·hn。注意，由于条件不满足，我们有α1。4.3Runge-Kutta-Fehlberg 4/5阶方法给定某一阶的数值方法，可以使用任何其他高阶的数值方法来获得局部误差的估计。然而，在每个时间步长中使用第二方法计算第二近似可能在计算上是昂贵的[1]。这个问题可以通过使用共享函数值的方法来避免，这些方法被称为嵌入对。Runge-Kutta-Fehlberg45阶方法（RKF 45）[8]利用了这种嵌入对。它使用五阶方法来估计四阶方法的局部误差。在每个步骤中，对于四阶方法的近似，必须计算5个值（斜率），用于计算yn+1作为加权和。用于误差估计的五阶方法需要6个斜率值。然而，其中5个已经通过四阶方法计算，因此仅需另外确定一个斜率。计算5阶近似yn+1以估计4阶近似yn+1的局部误差。然而，由于高阶方法比低阶方法得到更精确的 结果， 所 以 我们用y_n+1代替y_n+1作为近似结果。这种技术称为局部外推。5自适应步长法在热力系统建模中本节概述了基于RKF 45方法的自适应步长技术集成到我们的建模框架中，以支持实时Maude中具有交互组件的混合系统的形式化建模和分析图3显示了全球框架。[4]请注意，p的计算可以重用p的大部分计算，参见S e ction4.3。24M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17时间可以前进时间的经过E/F-NM执行连续行为步长连续行为时间无法前进执行离散行为离散行为误差容限E/F-NM误差计算步长公差误差，接受步长误差超出公差，拒绝步长减小步长增加步长估计误差E/F-NM作用力/流量数值方法计算图3.第三章。具有自适应步长的物理系统模型的执行5.1热系统的实时建模我们举例说明我们的方法热系统如图1所示1.一、热系统中的物理实体是热实体，物理相互作用是热的交互. 热实体的温度根据T温度变化。˙=100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000m·c其中，ΔQ是连接的热相互作用的热流速之和m是物体的质量，c是它的热容。因此，热传导率QM. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）1725L通过传导的两个实体之间的距离由Qstec=k·A·（T1−T2）定义，其中T1和T2是相互作用的实体的当前温度，k、L和A分别是导热率、厚度和通过导热率使热量从其流出我们在Real-TimeMaude中将热实体建模为以下类ThermalEntity：类ThermalEntity|温度：Rat，模式：CompMode，我屁股：PosRat， heatCap：PosRat，temp-p：Rat， temp-o1：Rat，temp-o2：大鼠。e对象变量temperature表示对象的温度。属性模式用于区分连续动力学的不同模式（见下文）。属性mass和heatCap分别表示实体的质量和热容。temp-p、temp-o 1、temp-o2是用于RKF 45方法计算的辅助属性。实体我们可以将更多特定类型的热实体定义为基类ThermalEntity的子类。例如，下面的类WaterEntity表示水物质：WaterEntity类|phase：MatterState，heatTrans-p：Rat，heatTrans-o1：Rat，heatTrans-o2：Rat。子类WaterEntity< ThermalEntity。排序MatterState。ops液体固体气体熔化蒸发冷凝冷冻：-> MatterState。ops defaultphaseTrans：-> CompMode。属性相表示水物质的相，其可以是固体、液体、气体的主要相之一，或者是熔化、冻结、26M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17蒸发或冷凝。当温度达到给定值时，发生从主相到相变的变化，而当相变期间积累的热量除以实体的质量达到称为潜热的给定值时，发生从相变到主相的变化。属性heatTrans存储相变中水的累积热量。其余的属性是计算近似值所必需的。该模式决定了连续动力学的计算模式。对于水，温度的连续动态在所有三个主要阶段是相同的，而温度在相变期间不改变。除了主阶段的默认计算模式外，我们还为相变添加了模式phaseTrans每个相位变化由瞬时重写规则建模。我们展示了水的八条规则中的两条：crl [固体至熔化]：< E：水实体|温度：T， 相：固体>=> ifT>= 0. crl [熔化成液体]：< E：水实体|阶段：熔化，heatTrans： QT，质量：M>=>< E：WaterEntity|phase：liquid，mode：default> if QT / M >= latentHeatFusion.“热相互作用”对热实体之间的热传递进行建模。例如传导、对流和辐射。我们定义了一般热相互作用的类别和三种热传递机制的子类类热相互作用|实体1：Oid，实体2：Oid，hfr：大鼠，面积：PosRat，hfr-p1：大鼠，hfr-p2：大鼠，hfr-p3：大鼠，hfr-p4：大鼠，hfr-p5：大鼠。类传导|thermCond：PosRat，厚度：PosRat。对流类|convCoeff：PosRat。类辐射|发射：PosRat。子类传导对流辐射热相互作用。 NumMethod[ctor]。ops adj1 adj2：-> CompStepSize [ctor].ops static dynamic：-> StepSizeType [ctor].ops eps epus：-> ErrorControlType [ctor].SysMan类|numMethod：NumMethod，stepSizeDef：Rat，stepSizeCur：Rat，stepSizeType：StepSizeType，errorTol：Rat，compStepSize：CompStepSize，safetyFactor：Rat，limitStepSize：Bool，stepSizeMin：Rat，stepSizeMax：Rat，limitAdjustRate：Bool，adjustRateMin：Rat，adjustRateMax：Rat，5.我们不显示变量声明;相反，我们遵循Maude约定，变量以大写字母书写，函数符号（包括常量）以小写字母开头M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）1727errorControl：ErrorControlType，localExtrapolation：Bool.属性numMethod指定使用哪种数值方法。attributestepSizeDef存储初始步长，stepSizeCur存储当前步长。stepSizeType决定使用固定步长还是自适应步长。errorTol定义了自适应步长计算中的误差容限（假设我们使用单个容限值）。compStepSize定义使用哪safetyFactor定义了局部最优步长的一部分，可用于减少近似误差。limitStepSize、stepSizeMin和stepSizeMax限制步长的值。limitAdjustRate、adjustRateMin和adjustRateMax用于限制步长的增大或减小速率 。 errorControl 选 择 每 步 误 差 或 每 单 位 步 误 差 来 控 制 步 长 。localExtrapolation指定是否在数值计算中使用外推技术RKF 45方法在热实体的属性temp-o 1和temp-o2中存储通过四阶和五阶方法得到的温度值的近似值函数maxError计算系统中所有热实体的最大局部误差估计：opmaxError：Configuration -> Rat.int maxError（< E：ThermalEntity |temp-o1：TEMP-O1，temp-o2：TEMP-O2，mode：default> REST）=max（abs（TEMP-O1-TEMP-O2），maxError（REST））。eq maxError（CONFIG）= 0[owise]。adjustRate函数使用每步误差计算步长调整的因子（我们有一个类似的每单位步长误差函数op adjustRate：CompStepSize Rat Rat ErrorControlType -> Rat。eqadjustRate（adj1，ERR，ERRTOL，SAF，eps）= SAF * root5（ERRTOL/ERR）。1函数root 5（X）将X5计算为exp（1/ 5· ln（X））。函数stepSizeRKF基于RKF 45方法计算步长。 如果最大局部误差低于容差值，则返回一对值，包括当前步长和下一个时间步长的步长如果没有应当说明函数在以较小的步长计算新的近似值后被递归调用。当对步长修改没有限制时，以下等式定义了该函数：op stepSizeRKF：Configuration -> ErrorStepSize.09 - 01张晓波（< SM：SysMan |compStepSize：ADJ，stepSizeCur：SSCUR，errorTol：ERRTOL，safetyFactor：SAF，limitStepSize：false，limitAdjustRate：false，errorControl：ERRCTR> REST）=如果ERR = ERRTOL，则 SSCUR; SSRKFelse stepSizeRKF（compute-EF-RKF 45（ REST））fiif ERR：= maxError（ REST）/\SSRKF：= adjustRate（ADJ，ERR，ERRTOL，SAF，ERRCTR）* SSCUR.我们还实现了一个类似的功能，限制步长变化的速率。以下刻度规则将系统中的时间提前stepSizeRKF计算的步长，并为所有热图元计算e排序变量的新值。如果使用外推法，这些值是5阶近似值，否则是4阶近似值crl [tick-adaptive-stepsize]： REST28M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17努力物理学第一次初始点努力值流物理学互动努力物理实验室2初始点努力值E/F-NM作用力/流量数值方法计算在这一点上努力是有价值的初始点流量值该点的流量值在这一点上努力是有价值的试验点的布局起点与终点之间终点的工作量值终点的工作量值见图4。 在努力/流量计算中数值方法适应的一般模型。=>delta（ REST）in time firstES（SSPAIR）如果TimeCanAdvance（REST）/\SSPAIR：= stepSizeRKF（compute-EF-RKF 45（ REST））。eq delta（REST）= compute-EF-RKF45-Order5（REST）。eq delta（REST）= compute-EF-RKF45-Order4（REST）。5.3集成RKF45方法在我们的e-类/e-类框架中调整数值方法的一般模型如图所示四、 我们使用时间离散化，并计算每个小的时间步长的近似值。 为了通过数值方法计算近似，必须计算一些斜率k1到kn。6对于RKF 45方法，我们需要6个斜率k1到k6，如第4节所述。对于每个ki，我们需要计算从某个初始点开始的小时间步长的行为的线性近似这是通过（1）首先计算在初始点的所有热相互作用的热流动速率，（2）对每个实体的所有连接相互作用的热流动速率求和，以及（3）线性地近似E_s，即。在小的时间步长之后的温度，假设计算的热气流速率恒定。由于空间有限，在下文中，我们仅限于解释k1的这些计算步骤（直到kn，其他情况类似，但使用不同的辅助属性）。函数computeFlow-IP根据[7]中描述的物理定律计算初始点的每个热交互的热流速。我们只展示热传导的情况opcomputeFlow-IP：配置->配置。cq-computeFlow-IP（REST）=computeFlow-IP（REST），如果QDOT-T：= Qdot-Conduction（K，L，A，T1，T2）。eqcomputeFlow-IP（CONFIG）= CONFIG [owise]。6在我们以前的工作中，我们已经将这种技术应用于欧拉、龙格-库塔二阶和龙格-库塔四阶方法。M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）1729ΣΣL·Mc上面的等式计算两个热实体E1和E2之间的热交互TI的初始热流动速率，然后递归地将 该 函 数 应用于 剩余的 配 置 。 函 数 Qdot-Conduction 将动 力 学 定 义 为Qstec=K·A·（T1−T2）。函数sumFlows-IP计算连接到热实体的所有热交互op sumFlows-IP：Configuration Oid -> Rat.2016 - 05 - 25 00：00：00< TI：热相互作用|实体1：E1，实体2：E2，hfr：QDOT > REST，E）= if（E == E1 or E == E2）then(ifE == E1则-1 *QDOT +sumFlows-IP（REST，E）否则QDOT +sumFlows-IP（REST，E）elsesumFlows-IP（REST，E）fi.等式sumFlows-IP（CONFIG，E）= 0 [owise]。函数computeEffort-P1在时间步长之后线性地近似系统中的每个热实体的温度，假设在时间步长上恒定的热流速率它调用表示连续动态的函数TdotgivenbyTtec=Qstec，whereeQstec是通过sumFlows-IP计算的实体的热相互作用的热流速值的总和，m是质量，c是热容。SM的属性numMethod和stepSize分别确定数值方法和时间步长：opcomputeEffort-P1：配置->配置。01 - 02< SM：SysMan|numMethod：mp，stepSize：H> REST）=computeEffort-P1（ REST）如果TEMP-P1：=TEMP+ 1/4 * H * Tdot（sumFlows-IP（REST，E），M，C）。等式computeEffort-P1（CONFIG）= CONFIG [owise]。6案例研究本节研究基于RKF 45方法的自适应步长技术的自适应如何影响热力系统仿真和时间分析的准确性和性能。我们先在房间里喝一杯热咖啡。然后我们加一个加热器，给被加热者提供恒定的热流。7实验在具有Intel（R）Pentium（R）4 CPU3.00 GHz和3 GB RAM的计算机上进行。可执行的正式模型，以及下面描述的模拟和分析命令，可在http://www.ifi.uio.no/RealTimeMaude/Coffee/上获得。6.1案例研究1：房间里的一杯咖啡我们首先对房间里的一杯热咖啡进行建模，如图1所示，将传导和对流作为热相互作用，并使用真实的物理参数。初始状态由管理数值计算的SysMan对象、coffee和room热实体对象以及两个模拟热流的热交互对象组成：[7]在分析中，我们使用每步误差和外推法进行计算。30M. Fadlisyah et al. /Electronic Notes in Theoretical Computer Science 274（2011）17咖 啡间100200300400500600700800时间00.040.0350.030.0250.020.0150.010.005咖啡-RKF 45咖啡-精确客房-RKF 45客房：精确相 对 （ 全 局 ） 误 差 （ %）步长8018016070140601205010080406030402020100 100 200 300 400 500 600 700800时间00 100 200 300 400 500 600 700 800时间图五、案 例 研 究 1 的仿真结果，误差容限为10 −3。等式cs1 ={<咖啡：WaterEntity|温度：70，热帽：coffeeHC，质量：coffeeMass，模式：默认，temp-p：0，temp-o 1：0，temp-o2：0，相：液体，热传输：0，热传输-p：0，热传输-o 1：0，热传输-o2：0>< 房间：ThermalEntity|温度：20，热帽：roomHC，质量：roomMass，模式：默认，temp-p：0，temp-o 1：0，temp-o2：0，< crCond：传导|实体1：scoffee，实体2：room，hfr：0，thermCond：k，面积：condArea，厚度：cupThick，hfr-p1：0，hfr-p2：0，hfr-p3：0，hfr-p4：0，hfr-p5：0>< crConv：对流|实体1：scoffee，实体2：房间，hfr：0，convCoeff：h，面积：convArea，hfr-p1：0，hfr-p2：0，hfr-p3：0，hfr-p4：0，hfr-p5：0>< sm：SysMan |numMethod：rkf45，stepSizeCur：INIT-TIME-STEP，stepSizeDef：INIT-TIME-STEP，stepSizeType：dynamic，errorTol：1/1000，compStepSize：adj1，safetyFactor：9/10，limitStepSize：false，stepSizeMin：1/10，stepSizeMax：5，limitAdjustRate：false，adjustRateMin：1/100，adjustRateMax：1/4，errorControl：eps，localExtrapolation：true>}。可以使用以下定时重写命令来模拟直到时间500的系统行为：Maude>（时间上的trew cs1< = 500。）图 5显示了使用误差容限10−3的 模拟 结果。左边的图图中的小图显示了每个时间步两个温度近似值的全局误差相对值的变化。八、右边的图表显示了步长的变化，随着时间的推移，步长越来越大下表比较了模拟时间为500时使用不同误差容限的模拟结果：误差容忍埃什奥尔特绝对误差（+ Rel %）CPU时间（s）MinMaxAvg10−3TcTr3.4741e-06（4.9815e-06）8.1800e-08（4.0930e-07）0.0101（0.0354）2.3796e-04（0.0011）0.0056（0.0162）1.3196e-04（6.3503e-04）410−4TcTr3.4741e-06（4.9815e-06）8.1800e-08（4.0930e-07）0.0