[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 transfer 5 units to account2. Creating account2
costs 1 unit for intrinsic gas and 1 unit transaction gas,
leavint account1 with balance 3.

Account 1 callling 'sendValue' in account 2 results:
- account1 paying for 1 unit for intrinsic gas + 1 unit transaction gas, and
receiving 1 unit from account 2. Resulting to balance 3 - 2 + 1 = 2.
- account2: sends 1 unit to account1, and pays 1 unit for intrinsic gas,
and 1 unit for transaction gas, resulting to balance 5 - 3 = 2
features/010-solidity/200-send.feature:26
# State space extract
#
# eth_accounts@1={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 0]}
# eth_accounts@2={[address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 10]}
# eth_accounts@3={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 3],
#                  [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 5] }
# eth_accounts@4={ [address |-> "d_eth_address_1", codeHash |-> Nil, balance |-> 2],
#                  [address |-> "d_eth_address_2", codeHash |-> "Demo1", balance |-> 2] }
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