[More Detail] [Collapse All]
Feature: Create two separate contracts
features/100-constructors/100-two-contracts.feature
- Background: Create configuration with two source files
link
features/100-constructors/100-two-contracts.feature:3
Given I create initial sbuilder context with:
Directory
solidity demo1
solidity demo2
setup setup1
# Content of solidity 'demo1'
Given a file named "solidity/demo1.sol" with:
pragma solidity >0.4.4;

contract Demo1 {

    uint storedData1;
    address owner1;

    function set(uint x) {
        storedData1 = x;
    }

    function get() constant returns (uint retVal) {
        return storedData1;
    }
}
# Content of solidity 'demo1'
And a file named "solidity/demo2.sol" with:
pragma solidity >0.4.4;

  contract Demo2 { 

    uint mem;
    function setter(uint x) {
        mem = x;
    }

  }
- Scenario: Create Demo1 and call setter
link
features/100-constructors/100-two-contracts.feature:51
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ethre value range, could be also int
     - domain: eth_value
       type: Int


     - domain: Demo2_mem
       values: 
           - arvo1
           - arvo2

     - domain: Demo1_storedData1
       values: 
           - store1_1
           - store1_2
           - store1_3


 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
              _default: 1
              value: 7
        - interface: Demo1()
          bindExact: true                    
          input:
              _default: 1
              sender: 1
              value: 3
        - interface: Demo1(set)
          bindExact: true
          input:
              x: store1_3
              sender: 1
              value: 0
              recipient: 2
              originator: 2
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Field Value
1 step p_personal_newAccount__
2 step p_geth_mine__
3 step p_Demo1__
4 step p_Demo1_set_
4 eth_storageRoot storedData1 "store1_3"
- Scenario: Fan out state space
link
features/100-constructors/100-two-contracts.feature:111
# Content of setup 'setup1'
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ethre value range, could be also int
     - domain: eth_value
       range: [0,7]


     - domain: Demo2_mem
       values: 
           - arvo1
           - arvo2

     - domain: Demo1_storedData1
       values: 
           - store1_1
           - store1_2
           - store1_3


 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
              _default: 1
              value: 7
        - interface: Demo1()
          # input:
          #     sender: 1
        - interface: Demo1(set)
          bindExact: true
          input:
              x: store1_3
              sender: 1
              value: 0
              recipient: 2
              originator: 2
        - interface: Demo2()
          input:
              sender: 1
        - interface: Demo2(setter)
          bindExact: true
          input:
              x: arvo2
              _default: 1
              sender: 1
              value: 0
              recipient: 3
              originator: 2
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Field Value
1 step p_personal_newAccount__
2 step p_geth_mine__
3 step p_Demo1__
4 step p_Demo1_set_
5 step p_Demo2__
6 step p_Demo2_setter_
4 eth_storageRoot storedData1 "store1_3"
5 eth_storageRoot storedData1 "store1_3"
6 eth_storageRoot storedData1 "store1_3"
6 eth_storageRoot mem "arvo2"