[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


Define 'demo1' solidity source and setup 'setup1'
create solidity source in 'solidity/demo1.sol',
and setup configuration in 'cnf/setup1.yaml'
features/050-ether-balance/100-mined-transfer-value.feature:3
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.4.4;

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

In this scenario, step
- 1: creates an account with address 'd_eth_address_1'
- 2: mines non-deterministally a value with range 0..3 to benenficary address 'd_eth_address_1'
- 3: account  'd_eth_address_1' creates Demo1 contract, and transfers value with range
  0..3 to the new created account 'd_eth_address_2'

Expect
- value mined -3..0
- balance 0..3 for account 'd_eth_address_1'
- balance 0..3 for account 'd_eth_address_2'


State space extract:

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

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

   eth_mined@2=-2
   eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 2]}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   eth_mined@3=-3
   eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0],
                    [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 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 Key Field Value
1 step p_personal_newAccount__
2 step p_geth_mine__
2 eth_mined 0
2 eth_mined -1
2 eth_mined -2
2 eth_mined -3
3 eth_accounts d_eth_address_1 balance 0
3 eth_accounts d_eth_address_1 balance 1
3 eth_accounts d_eth_address_1 balance 2
3 eth_accounts d_eth_address_1 balance 3
3 eth_accounts d_eth_address_2 balance 0
3 eth_accounts d_eth_address_2 balance 1
3 eth_accounts d_eth_address_2 balance 2
3 eth_accounts d_eth_address_2 balance 3