[More Detail] [Collapse All]
Feature: Solidity methods
features/010-solidity/200-send.feature
- Background: Define contract with methods
link
features/010-solidity/200-send.feature:4
Given I create initial sbuilder context with:
Directory
solidity Demo1
setup setup1
And a file named "solidity/Demo1.sol" with:
contract Demo1 {
    function Demo1()  {
    }

    function sendValue()  {
       msg.sender.send( 1 );
    }
}
- Scenario: Call msg.sender.send
link

Create account1, and mine 10 units to account1. Account1 creates
account2, and transfers 3 units to account2. Account 1 calls
account2 sendValue -method, which moves 1 unit to msg.sender.


Balances:

          acc1    acc2
step 2:   10        - 
step 3:    7        3
step 4:    8        2
features/010-solidity/200-send.feature:26
Given 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,10]

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

 - step-extension:
        - interface: personal_newAccount()
        - interface: geth_mine()
          bindExact: true
          input:
              _default: 1
              beneficiary: 1
              value: 10
        - interface: Demo1()
          bindExact: true
          input:
              _default: 1
              sender: 1
              value: 3
        - interface: Demo1(sendValue)
          bindExact: true
          input:
              _default: 1
              sender: 1
              recipient: 2
              value: 0
When I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
3 step p_Demo1__
4 step p_Demo1_sendValue_
2 eth_accounts d_eth_address_1 balance 10
3 eth_accounts d_eth_address_1 balance 7
3 eth_accounts d_eth_address_2 balance 3
4 eth_accounts d_eth_address_1 balance 8
4 eth_accounts d_eth_address_2 balance 2