| |
|
|
|
|
|
| |
|
|
| |
 |
Invoking Generation
|
|
|
Generation is required before we can do anything meaning full with e language. There are two ways of invoking generation. |
| |
|
|
|
|
- Generation is invoked automatically when generating the tree of structures starting at sys.
- Generation can be called for any data item by using the gen action.
|
| |
|
|
|
|
The generation order is (recursively): |
|
|
- Allocate the new struct.
- Call pre_generate().
- Perform generation
- Call post_generate().
|
| |
|
|
| |
 |
gen
|
|
|
This generates a random value for the instance of the item specified in the expression and stores the value in that instance, while considering all the constraints specified in the keeping block, as well as other relevant constraints at the current scope on that item or its children. Constraints defined at a higher scope than the enclosing struct are not considered. |
| |
|
|
|
|
The following considerations also apply. |
|
|
- Values for particular struct instances, fields, or variables can be generated during simulation (on-the fly generation) by using the gen action.
- This constraint can also be used to specify constraints that apply only to one instance of the item.
- The soft keyword can be used in the list of constraints within a gen action.
- The earliest the gen action can be called is from a struct's pre_generate() method.
- The generatable item for the gen action cannot include an index reference.
- If a gen ... keeping action contains a for each constraint, the iterated variable needs to be named.
|
| |
|
|
| |
 |
Example - gen
|
| |
|
|
|
|
1 <'
2 struct transaction {
3 address: uint;
4 };
5
6 extend sys {
7 tra : transaction;
8 run() is also {
9 for {var i : uint = 0; i < 2; i = i +1} do {
10 gen tra;
11 print tra;
12 };
13 };
14 };
15 '>
You could download file constrain_gen_ex17.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
tra = transaction-@0: transaction
---------------------------------------------- @constrain_gen_ex17
0 address: 1109997210
tra = transaction-@1: transaction
---------------------------------------------- @constrain_gen_ex17
0 address: 172288450
|
| |
|
|
|
|
|
| |
|
|
| |
|
pre_generate()
|
|
|
The pre_generate() method is run automatically after an instance of the enclosing struct is allocated, but before generation is performed. This method is initially empty, but can be extended to apply values procedurally to prepare constraints for generation. It can also be used to simplify constraint expressions before they are analyzed by the constraint resolution engine. |
| |
|
|
|
|
Note : Prefix the ! character to the name of any field whose value is determined by pre_generate(). Otherwise, normal generation will overwrite this value. |
| |
|
|
| |
|
Example - pre_generate()
|
| |
|
|
|
|
1 <'
2 struct a {
3 ! m: int;
4 m1: int;
5 keep m1 == m + 1;
6 pre_generate() is also {
7 m = 7;
8 };
9 };
10 extend sys {
11 A: a;
12 run() is also {
13 for {var i : uint = 0; i < 4; i = i +1} do {
14 gen A;
15 print A;
16 };
17 };
18 };
19 '>
You could download file constrain_gen_ex18.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
A = a-@0: a
---------------------------------------------- @constrain_gen_ex18
0 !m: 7
1 m1: 8
A = a-@1: a
---------------------------------------------- @constrain_gen_ex18
0 !m: 7
1 m1: 8
A = a-@2: a
---------------------------------------------- @constrain_gen_ex18
0 !m: 7
1 m1: 8
A = a-@3: a
---------------------------------------------- @constrain_gen_ex18
0 !m: 7
1 m1: 8
|
| |
|
|
| |
|
post_generate()
|
|
|
The post_generate() method is run automatically after an instance of the enclosing struct is allocated and both pre-generation and generation have been performed. You can extend the predefined post_generate() method for any struct to manipulate values produced during generation. The post_generate() method allows you to derive more complex expressions or values from the generated values. |
| |
|
|
| |
|
Example - post_generate()
|
| |
|
|
|
|
1 <'
2 struct a {
3 ! m: int;
4 m1: int;
5 post_generate() is also {
6 m = m1 + 1;
7 };
8 };
9 extend sys {
10 A: a;
11 run() is also {
12 for {var i : uint = 0; i < 4; i = i +1} do {
13 gen A;
14 print A;
15 };
16 };
17 };
18 '>
You could download file constrain_gen_ex19.e here
|
| |
|
|
| |
|
Compiler Output
|
| |
|
|
|
|
A = a-@0: a
---------------------------------------------- @constrain_gen_ex19
0 !m: 326332202
1 m1: 326332201
A = a-@1: a
---------------------------------------------- @constrain_gen_ex19
0 !m: 32481662
1 m1: 32481661
A = a-@2: a
---------------------------------------------- @constrain_gen_ex19
0 !m: 1655552526
1 m1: 1655552525
A = a-@3: a
---------------------------------------------- @constrain_gen_ex19
0 !m: 91542956
1 m1: 91542955
|
| |
|
|
| |
|
|
| |
|
|
|
|
|
| |
|
|
