Dvlab Open WikiTicc provides the functionality to do random simulation. The following is the signature of the simulate function with a description of its parameters:
val simulate : symbolic_module_t -> string -> int -> string -> unit Parameter 1 is a Ticc module Parameter 2 is an expression representing the starting state Parameter 3 is the number of cycles to simulate Parameter 4 is the name of the file that should contain the simulation results
Specifying the Starting State
The starting state can be any valid Ticc expression. Please refer to the Input Grammar for expression syntax. The expression is not required to specify values for all variables in the symbolic module. Ticc will compute a starting state, as an assignment over all variables, by first restricting the input and output invariants to the user specified starting state and then picking a random minterm from that restricted set.
If the user specified starting state violates the input or output invariants the simulation session will terminate.
The Random Simulation Algorithm
Ticc randomizes over all available rules that can be applied from a given state. The set of rules that can be applied from a given state is computed from the set of all available rules by ensuring that the next state for each such rule does not violate either the input or the output invariants. Once a rule is picked at random from the set of applicable rules, the next state is computed and a random minterm, providing an assignment over all variables in the module, is picked to be the next state.
Simulation Output Format
Ticc generates an HTML file with the results of simulation. The following is a snippet from the HTML generated for the tutorial/buffered_receiver example.
Simulation Report Inputs ------ Module: Buffer*Receiver nCycles: 16 User initial state: "Receiver.busy & Buffer.msgs < 2" Computed Start State -------------------- Variables: Buffer.msgs Receiver.busy Values: 0 1 Simulation ---------- Cycle Action Name Buffer.msgs Receiver.busy ----- ----------- ----------- ------------- 1 proc 0 0 2 delta_env 0 0 3 snd 1 0 ...
The "Inputs" section shows the inputs given to the simulate function. The "Computed Start State" section shows the starting state computed by Ticc using the user starting state expression and the input and output invariants. Under the "Simulate" section, each simulation cycle shows the cycle number, the action randomly chosen and the values of the variables for that simulation cycle.