[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

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:
features/050-ether-balance/100-mined-transfer-value.feature:68
# 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] }
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