计算机仿真技术 作者 郝培锋 崔建江 潘峰 第8章1.pptVIP

* * * 2 * 4 15 * 火车在距道口一定距离时通知控制中心其即将到达。 控制中心通知道口关闭 关闭（或打开）道口需要一定时间 火车通过道口后通知控制中心其已离开 控制中心通知道口打开 controller gate approach lower exit raise near far far crossing chan approach,exit,raise,lower; clock waiting_time; const a 5,b 3,c 2; //const a 5,b 4,c 2; //const a 5,b 3,c 3; A[] (train.crossing imply gate.down) A[](not gate.up imply waiting_time=10) 对于仿真模型的校核、验证与认可的工作一般贯穿于整个仿真过程，由于仿真规模的不断扩大，目前已经考虑了系统的校核、验证与认可。利用仿真系统进行对实际的分析和研究，进而实现对实际系统的预测和辅助决策，保证仿真模型在计算机上的正确运行，十分重要和必要。随着实际对仿真的需求，仿真技术的不断发展，仿真模型涉及的范围越来越广，复杂程度也将大为增加，仿真模型的校核、验证与认可的方法也会不断发展。 * * * * * * * * * * * * * * * * * * * * * * * * * Clock constraints Location invariants States x=5 ? y3 n m a x := 0 x=5 y=10 Location invariant Location invariant Transitions x=5 ? y3 n m a x := 0 x=5 y=10 label, 同步标号 guard, 使能条件 reset, 时钟重置 g; a; ? g 是使能条件, a 是同步标号, ? 是该迁移要重置的时钟的集合. x=5 ? y3 n m a x := 0 x=5 y=10 1. Discrete transitions 2. Delay transitions ( n , x=2.4 , y=3. 5 ) ( n , x=3.5 , y=4.6 ) 1.1 ( n , x=2.4 , y=3.5 ) ( m , x=0 , y=3.5 ) a 满足不变量 定义. A timed automaton A is a tuple L,L0,?, X,I,E, where 1). L is a finite set of locations, 2). L0 ? L is a set of initial locations, 3). ? is a finite set of synchronization labels, 4). X is a finite set of clocks, 5). I: L?C(X) is a mapping from locations to clock constraints, and 6). E?L?C(X) ?? ?P (X) ? L is the set of transitions. L={off,on}, L0={off}, ?={press}, X={x} I={off ? true, on?x=2} E={(off,true,press,{x},on),(on,x=2, ?,?,off)} Off on press X=2 X=2 X:=0 定义. 设 是一个TA, A的语义是如下定义的一个LTS: T由下面的两种迁移构成 -- Delay transitions: -- Discrete transitions: 设 (i=1,2)是两个时间自动机，且 则 是如下定义的一个时间自动机 实时性质 有界响应性。如：若p发生，则q必在２个时间单位内发生。 有界安全性。如：若p发生，则q在２个时间单位内不会发生。 ….. 在时序逻辑中引进时间表达能力的方式 引入有界时序算子。 　如 引入（全局）时钟变量T，其值(非严格)单调递增。