Before the lab classes: prepare HML file, which contains a complete ARD model of the system designed in the previous lab classes.

• For more information, read the following articles:
  • XTT2 Method
  • ALSV(FD) Logic
  • Attribute Specification
• The XTT design is supported by HQed tool.

• Run the HQEd tool:

  ~kinio/hades/hqed/hqed

Having a complete ARD model of a system, the next step is to generate a XTT preliminary model. It can be done by:

• Load a prepared ARD model into HQEd.
• The editor will automatically switch into ARD mode and display the model.
• HQEd allows for viewing of all the ARD levels simultaneously as well as the TPH diagram.
• In order to generate a preliminary XTT model select Create XTT action from XTT menu.
• When the XTT schema is generated successfully, the editor displays the appropriate message.
• In case of some errors, the ARD model must be checked.

The types defining is a one of the most important steps during the design. The automatically generated model has defined only a one type named default, which is related with all attributes. The appropriate definition of the types allows for full exploiting of the Hekate advantages from the formal verification point of view.

• In order to create a new type, run the Type Manager dialog by clicking the action Types → Type manager.
• Then press New… button.
• Fullfill all the fields in the new window dialog.
• In order to define a domain of the type:
  • Typ ograniczeń: domain
  • select the domain value in the Contraints type filed and
  • press Edit button.
• Kolejne okna dialogowe które będą się pojawiały zależą od rodzaju typu podstawowego. Przy ich pomocy należy wprowadzić odpowiednie wartości w celu zdefiniowania dziedziny,
• The layout of the next dialog windows depends on the several factors, which are not here described.
• For the Cashpoint example the following types must be defined:

The complete ARD model should contain all the attributes, which describe the system, and dependencies between them. However, it does not contain any information about types. This is due to the fact, that neither of tools VARDA nor HJEd do not support types defining. Thus, the next step is to define attributes type and the other properities.
The following table contains all the attributes that should be defiend. The last column contains an optional attribute description.

Definiowanie reguł jest najważniejszym elementem tej fazy projektowania. Otrzymany na bazie modelu ARD diagram XTT zawiera tylko nagłówki tabel, które winny zostać wypełnione regułami oraz uzupełnione o odpowiednie połączenia. Poniżej znajduje się lista reguł, które należy zdefiniować w modelu XTT systemu bankomat. W poniższych regułach przejęto nazwy atrybutów z poprzedniego ćwiczenia.

Rules defining is the most important stage of the design. The ARD model provides only the schemas (headers) of the XTT tables, which must be filled with rules. Below the list of all rules, which must be defined, can be found:

• This table calculates the difference between entered and correct PIN.
• The table schema:

• The table contains only one rule that calculates the difference:

• This table determines the system behaviour after PIN checking:
• The table schema:

• The table contains two rules that determine the system behaviour in case when the entered PIN is correct as well as incorrect.
  • When the entered PIN is incorrect:

• When the entered PIN is correct:

• The both tables have very a similar functionality. They check if the money withdrawal is possible. This can be done when:
  • the required amount of money does not exceed the amount on the user account, and
  • the required amount of money does not exceed the amount in the ATM.
• The following example presents the table definition, which checks if the user's required amount of money does not exceed the amount on his account. The definition of the second table differs with the name of the attribute.
• The table schema:

• The table contains only one rule:

• This is the final table, which defines the output from the system.
• The table schema:

• The table contains six rules:

After the rules design stage, the model must be complemented by defining the connections between tables. Usually, all the rules in the given table are connected to the same table. The connection of the first rule is determined by ARD→XTT transition algorithm.

The HQEd tool allows for defining of initial states in the States panel.

• Click on the empty area with the help of RMB and choose Add new state group action.
• The dialog window allows for defining a name of the group of states as well as the set of attributes initializing in this group.
• When all is ready then click OK.
• In the state panel a new states group appears.
• In the same manner as XTT tables cells, the initial values of the attributes can be defined.
• During this lab classes at least two states that differs with system response must be defined.

Before the physical implementation, the simulation of the system can be performed. The simulation can be executed by built-in engine or with the help of external plugin. During the calsses at least one type of simulation should be done for at least two different initial states.
The simulation can be performed by:

• In the states panel find the required state.
• Click with RMB in the row corresponding to this state and in the column label.
• From the context menu select Start simulation from this state and from the submenu the required inference engine.
• After the simulation that apropriate row of the output table should be updated to the value that is a response of the system on the selected initial state.
• The line of the connection between state table and output table should be changed into dashed.
• Click on this connection in order to highlight all the fired rules during the inference process.
• In addition in the Execute messages tab the details of the simulation can be found.

• Having a complete XTT model, a physical implementation (in the form of HMR file) can be generated:
  • Choose Generate HMR code action from Execute menu.
  • Save the file.
  • Note that on the Linux-based systems the file extension (hmr) must be provided as well.

Z braku lepszego miejsca tutaj studenci wpisują komentarze natury ogólnej do tego lab.

Definiowanie reguł nie ma szczegolowej instrukcji jak to ustawic Program sie zawieszaa:) nie ma w instrukcji zeby zapisac, a program sie zawiesza. Po restarcie brakuje tabel na dane wejsciowe Zamiast wpisywac recznie wszystkie typy, ciekawiej byloby to udostepnic do importu a moze w zamian pokazac 2-3 reguly i kazac jakas jedna samemu wymyslec?

naglowek Definiowanie atrybutów i Definiowanie typow sa zamienione:)