[More Detail] [Collapse All]
Feature: Use non-deterministic choice in setup
features/050-ether-balance/100-mined-transfer-value.feature
- Background: Start with empty context and create configuration
link
features/050-ether-balance/100-mined-transfer-value.feature:3
#
# Define 'demo1' solidity source and setup 'setup1'
# create solidity source in 'solidity/demo1.sol',
# and setup configuration in 'cnf/setup1.yaml'
#
Given I create initial sbuilder context with:
Directory
solidity demo1
setup setup1
# Solidity contract 'Demo1' in file 'solidity/demo1.sol'
And a file named "solidity/demo1.sol" with:
pragma solidity ^0.3.5;

contract Demo1 {

    uint storedData;
    address owner;

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

    function get() constant returns (uint retVal) {
        return storedData;
    }
}
# Setup 'setup1'
And a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 3

       # Ether value range - later used non-deterministic choice
     - domain: eth_value
       range: [0,3]

       # TODO: should be created automatically
     - domain: eth_code_hash
       values:
          - Demo1
          - Demo2


    #
    # Two steps: first step creates an account, second step model
    # mining ether to this account

 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
        - interface: Demo1()
- Scenario: Non-deterministic choice
link

 One single command genaretes, pcal translates, and model checks

 Non-determistically mines values 0..3, and send value 0..3 when
 creating contract. However gasUsed will allways stays below 2
 (because only one Demo1() transaction is made, consuming 1 unit
 of intrinsic gas, and 1 unit trasnaction gas).

 State space extract shows all possible combination for mining value -3..-1,
 and creating a contract 'Demo1' with value 0..3.

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0]}
        eth_gasUsed@3=0
        eth_mined@3=0

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 1]}
        eth_gasUsed@3=0
        eth_mined@3=-1

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 2]}
        eth_gasUsed@3=0
        eth_mined@3=-2

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 3]}
        eth_gasUsed@3=0
        eth_mined@3=-3

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0]}
        eth_gasUsed@3=1
        eth_mined@3=-1

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 1]}
        eth_gasUsed@3=1
        eth_mined@3=-2

        step@3="p_Demo1__"
        eth_accounts@3={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 2]}
        eth_gasUsed@3=1
        eth_mined@3=-3

        step@3="p_Demo1__"
        eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
                         [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 0] }
        eth_gasUsed@3=2
        eth_mined@3=-2

        step@3="p_Demo1__"
        eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 1],
                         [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 0] }
        eth_gasUsed@3=2
        eth_mined@3=-3

        step@3="p_Demo1__"
        eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
                         [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 1] }
        eth_gasUsed@3=2
        eth_mined@3=-3
features/050-ether-balance/100-mined-transfer-value.feature:68
Given 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 eth_accounts balance 0
3 eth_accounts balance 1
3 eth_accounts balance 2
3 eth_accounts balance 3
3 eth_mined 0
3 eth_mined -1
3 eth_mined -2
3 eth_mined -3
3 eth_gasUsed 0
3 eth_gasUsed 1
3 eth_gasUsed 2