[More Detail] [Collapse All]
Feature: Configuration step-by-step walktrough

Define detailed configuration
- sbuilder.init
- create files:
    -- cnf/sbuilder.yaml
    -- cnf/setup1.yaml
    -- solidity/demo1.yaml

 - run
    -- sbuilder.rb generate setup1
    -- java -cp $TLATOOLS pcal.trans model
    -- java -cp $TLATOOLS tlc2.TLC setup
features/001-smoke/001-basic-configuration.feature
- Background: Start with empty context and create configuration
link
features/001-smoke/001-basic-configuration.feature:15
#
# Initialize direcotory structures
Given the following directories should not exist:
directory
cnf
src
gen
cache
And I run `bundle exec sbuilder.rb init`
Then the exit status should be 0
And the following directories should exist:
directory
cnf
src
gen
cache
#
# In cnf directory sbuilder.yaml & setup1.yaml
#
Given a directory named "cnf" should exist
And a file named "cnf/sbuilder.yaml" with:
extend:
  loaders:
     - className: Sbuilder::Ethereum::Plugin
       gem: sbuilder-ethereum
       configuration:
         solc_command: '../../bin/solc'
       objects:
          - objectName: solcLoader
            configuration:

interfaces:
    -  objectName: solcLoader
       url: solidity/demo1.sol

snippets:

  -  objectName: solcLoader
     snippets:

setups:
    - setupDirectory: setup1
      extensions:
        -  url: cnf/setup1.yaml

invariants:
    - accounts_type: account type valid
    - accounts_unique: unique entries in account state variable
    - accounts_valid: account id valid && account value valid
    - total_value: SUM( accounts.balance ) + mined must be 0
And a file named "cnf/setup1.yaml" with:
 - domain-extension:

     - domain: eth_address
       cardinality: 1

     - domain: eth_value
       type: Int

 - step-extension:
        - interface: personal_newAccount()
#
# Create solidity source files
#
Given a directory named "solidity"
And a file named "solidity/demo1.sol" with:
pragma solidity >0.4.4;

contract Demo {

    uint storedData;
    address owner;

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

    function get() constant returns (uint retVal) {
        return storedData;
    }
}
- Scenario: Generate, translate, and check
link

 Interface 'personal_newAccount()' corresponding process
 'p_personal_newAccount' should be found as well as interface
 'Demo(set)' 'p_Demo_set'.
features/001-smoke/001-basic-configuration.feature:113
Given I translate solidity to Tla with `sbuilder.rb generate setup1`
And the file "gen/setup1/tla/model.tla" should contain "fair process (p_Demo_set_"
And the file "gen/setup1/tla/model.tla" should contain "fair process (p_personal_newAccount"
And I cd to "gen/setup1/tla"
And I run pcal translation with `java -cp $TLATOOLS pcal.trans model`
And I check correctness with `java -cp $TLATOOLS tlc2.TLC setup`
- Scenario: Option --filter_src option prunes generated code
link

 Prune TLA model to include only snippets, which are reachable from
 from the step in current setup.

 Interface 'personal_newAccount()' corresponding process
 'p_personal_newAccount' called --> process should be found in
 model.tla.

 Interface 'Demo(set)' corresponding process 'p_Demo_set' NOT
 called --> process should NOT be found in model.tla.
features/001-smoke/001-basic-configuration.feature:128
Given I translate solidity to Tla with `sbuilder.rb generate setup1 --filter-src`
And the file "gen/setup1/tla/model.tla" should not contain "fair process (p_Demo_set_"
And the file "gen/setup1/tla/model.tla" should contain "fair process (p_personal_newAccount"
And I cd to "gen/setup1/tla"
And I run pcal translation with `java -cp $TLATOOLS pcal.trans model`
And I check correctness with `java -cp $TLATOOLS tlc2.TLC setup`