[More Detail] [Collapse All]
Feature: Conditional statements
features/010-solidity/100-expressions.feature
- Background: Define contract with functions
link

Functions
- ifTrue - return true
- ifFalse - return false
features/010-solidity/100-expressions.feature:5
Given I create initial sbuilder context with:
Directory
solidity Demo1
setup setup1
And a file named "solidity/Demo1.sol" with:
pragma solidity ^0.3.5;

contract Demo1 {
    uint public mostSent;

    function Demo1()  {
        mostSent = msg.value;
    }

    function ifTrue() returns (bool) {
        if (true) {
            return true;
        } else {
            return false;
        }
    }

    function ifFalse() returns (bool) {
        if (false) {
            return true;
        } else {
            return false;
        }
    }

    function ifIntLessThan() returns (bool) {
        if (1 < 2 ) {
            return true;
        } else {
            return false;
        }
    }

    function ifIntNotEqual() returns (bool) {
        if (1 != 2 ) {
            return true;
        } else {
            return false;
        }
    }

    function ifIntEqual() returns (bool) {
        if (1 == 1 ) {
            return true;
        } else {
            return false;
        }
    }

    function ifIntLessThanOrEqual() returns (bool) {
        if (1 <= 2 ) {
            return true;
        } else {
            return false;
        }
    }

    function setMost4() {
        mostSent = 4;
    }

    function ifMostGreaterThan4() returns (bool) {
        if ( mostSent > 4 ) {
            return true;
        } else {
            return false;
        }
    }


    function ifSend() returns (bool) {
        if ( msg.sender.send(msg.value ) ) {
            return true;
        } else {
            return false;
        }
    }


    function ifSend2() returns (bool) {
        if ( !msg.sender.send(msg.value ) ) {
            return true;
        } else {
            return false;
        }
    }


}
- Scenario: If with constant expressions
link
features/010-solidity/100-expressions.feature:111
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
       type: Int

    #
    # 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:
                value: 100
                beneficiary: 1
        - interface: Demo1()
          bindExact: true
          input:
                sender: 1
                originator: 1
                value: 50
        - interface: Demo1(ifTrue)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifFalse)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifIntLessThan)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifIntNotEqual)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifIntEqual)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifIntLessThanOrEqual)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(setMost4)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifMostGreaterThan4)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
Given I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Field Value
4 step p_Demo1_ifTrue_
4 responses response TRUE
5 step p_Demo1_ifFalse_
5 responses response FALSE
6 step p_Demo1_ifIntLessThan_
6 responses response TRUE
7 step p_Demo1_ifIntNotEqual_
7 responses response TRUE
8 step p_Demo1_ifIntEqual_
8 responses response TRUE
9 step p_Demo1_ifIntLessThanOrEqual_
9 responses response TRUE
10 step p_Demo1_setMost4_
11 step p_Demo1_ifMostGreaterThan4_
11 responses response FALSE
- Scenario: If with function return check
link
features/010-solidity/100-expressions.feature:221
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
       type: Int

    #
    # 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:
                value: 100
                beneficiary: 1
        - interface: Demo1()
          bindExact: true
          input:
                sender: 1
                originator: 1
                value: 50
        - interface: Demo1(ifSend)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
        - interface: Demo1(ifSend2)
          bindExact: true
          input:
                sender: 1
                recipient: 2
                originator: 1
                value: 0
Given I generate, translate, and model check setup `setup1`
Then State space extract `gen/setup1/tla/state.dump` contains
Tick Variable Key Field Value
4 step p_Demo1_ifSend_
4 responses i_Demo1_ifSend_ response TRUE
5 step p_Demo1_ifSend2_
5 responses i_Demo1_ifSend2_ response FALSE