Đang chuẩn bị liên kết để tải về tài liệu:
Model-Based Design for Embedded Systems- P49

Không đóng trình duyệt đến khi xuất hiện nút TẢI XUỐNG Tải xuống

Model-Based Design for Embedded Systems- P49: This book contains information obtained from authentic and highly regarded sources. Reasonable efforts have been made to publish reliable data and information, but the author and publisher cannot assume responsibility for the validity of all materials or the consequences of their use. | 456 Model-Based Design for Embedded Systems 14.3.5.1 Derived Functions and Logic Programs A query reduces some property of a model to a boolean value Either the property holds the query is satisfied or it does not hold. Sometimes this reduction loses information that should persist. For example suppose we want to know which states can be reached after one two and three FIGURE 14.8 Calculating reachable states from initial state 0. transitions of a FSM as shown in Figure 14.8. This can be done with the queries shown in Figure 14.9. Notice that the query findTwo which finds all states after two steps must first discover all the states one step away. Similarly the findThree query must find the states reachable in one and two steps before finding the states reachable in three steps. The Nth find query does all the work of the N 1 previous queries which is wasteful and makes the queries unnecessarily verbose. This problem can be solved by temporarily storing the results of queries into data structures. These temporary results are created using derived functions. A derived function is a function beginning with a lowercase letter. Derived functions are only used to temporarily remember some intermediate results and can never appear in the data elements of an input model. For example reachl state State . 14.29 declares a derived function for remembering those states reachable from an initial state after one step. Temporary results are created by writing the following expression reachl y x is Initial y is State t is Transition t.current x.state t.next y. Queries searching for reachable states 3. findOne x is Initial y is State 4. t is Transition 5. t.current x.state t.next y. 7. findtwo x is Initial y is State 8. t is Transition s is Transition 9. t.current x.state t.next s.current s.next y. 11. findThree x is Initial y is State 12. t is Transition s is Transition u is Transition 13. t.current x.state t.next s.current 14. s.next u.current u.next y. FIGURE 14.9 Queries for .