Readme Releases Todo

tla-parser-s - TLA+ language parser (for tla-sbuilder) - $Release:0.2.5$

A Ruby library for parsing TLA+ language.

Usage

Command line interface

Run

bin/tla-resolver.rb resolve v_pets --dir-globs demo/*

to parse files in demo/*, and to output

demo/state_pet.tla

because v_pets in defined in module state_pet.tla

Run

bin/tla-resolver.rb resolve enter_pet --dir-globs demo/*

to parse files in demo/*, and to output

demo/transaction_enter_pet.tla
demo/state_pet.tla

because enter_pet macro defined in demo/transaction_enter_pet.tla uses also variable definition v_pets defined in demo/state_pet.tla.

Api usage

require 'tla-parser-s'       # TLA+ parser && resolver

# create new context resolver
resolver =  TlaParserS::Resolver.new( options )

# Add Globals some constant symbols to resolver (to avoid unresolve warnings)
GLOBALS = %w( TRUE FALSE Cardinality)
resolver.initContext( GLOBALS )

# parse snippets in dir '"demo/**./*"'
snippet_files = Dir.glob( "demo/**./*" ) 
resolver.initSnippets( snippet_files ) do |status, entry|
    if ! status
        warn "Error parsing #{entry} - continue"
    end
    # continue
    true
end

# resolve depencies
depencies = resolver.resolveModules( getEntryPoints ) do |type,arr|
    case type
    when "start"
    when "resolved"
    when "unresolved"
    else
        raise "Unkown type #{type}"
    end
end

# dendencies of 'getEntryPoints' array
depencies