[More Detail] [Collapse All]
Feature: Use setup to control state space explosion
features/001-smoke/100-condesed-configuration.feature
- Background: Start with empty context and create configuration
link
features/001-smoke/100-condesed-configuration.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
setup setup2
# Content of solidity 'demo1'
And a file named "solidity/demo1.sol" with:
pragma solidity ^0.3.5;

contract Demo {

    uint storedData;
    address owner;

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

    function get() constant returns (uint retVal) {
        return storedData;
    }
}
- Scenario: Fixing state space
link

In this setup geth_mine fixes value 3, and the state space
shows balance with values 0 and 3 for time tick 2. Value 3 was
fixed as input value. Balance 0 results from the fact that
account to receive mined value was not fixed, and TLA tools
used also value Nil for an account address, which resulted no
value to be mined.


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

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

step@2="p_geth_mine__"
eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 3]}
features/001-smoke/100-condesed-configuration.feature:39
Given a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 1

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

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

 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          input:
              value: 3
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Regexp
1 step p_personal_newAccount__
2 step p_geth_mine__
2 eth_accounts balance 0
2 eth_accounts balance 3
- Scenario: Non-deterministic choice
link

Define a setup, which  non-determistically mines values
0..5 to balance for beneficiarry address.

 Results to state space extract:

 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0]}
 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 1]}
 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 2]}
 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 3]}
 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 4]}
 eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 5]}
features/001-smoke/100-condesed-configuration.feature:93
When a file named "cnf/setup2.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 1

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

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

 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
Given I generate, translate, and model check setup `setup2`
Then State space extract `gen/setup2/tla/state.dump` contains
Tick Variable Regexp
1 step p_personal_newAccount__
2 step p_geth_mine__
2 eth_accounts balance 0
2 eth_accounts balance 1
2 eth_accounts balance 2
2 eth_accounts balance 3
2 eth_accounts balance 4
2 eth_accounts balance 5