CSPM-cspm 0.8.0.0 → 0.8.1.0

raw patch · 15 files changed

+1151/−52 lines, 15 filesdep −prettydep ~CSPM-CoreLanguagedep ~CSPM-FiringRulesdep ~CSPM-FrontendPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: pretty

Dependency ranges changed: CSPM-CoreLanguage, CSPM-FiringRules, CSPM-Frontend, CSPM-Interpreter, CSPM-ToProlog, cmdargs, syb, transformers

API changes (from Hackage documentation)

Files

• CSPM-cspm.cabal +39/−47
• LICENSE +1/−1
• README.md +29/−0
• demo/lua/cspmPrelude.lua +66/−0
• demo/lua/ilua.lua +380/−0
• demo/lua/strict.lua +38/−0
• demo/lua/trace.lua +50/−0
• include/lua/bootstrap.lua +2/−0
• include/lua/cspmPrelude.lua +65/−0
• include/lua/demo.lua +48/−0
• include/lua/ilua.lua +380/−0
• include/lua/init.lua +3/−0
• include/lua/strict.lua +38/−0
• src/CSPM/LTS/LTS.hs +4/−4
• src/Scripting/LuaUtils.hs +8/−0

@@ -1,63 +1,56 @@ Name:                CSPM-cspm-Version:             0.8.0.0+Version:             0.8.1.0  Synopsis:            cspm command line tool for analyzing CSPM specifications. Description:   cspm is a small command line tool for analyzing CSPM specifications.-  It supports serveral modes of operation.-  For example as:-  .-  * 'cspm --help'      -> print a help message.-  .-  * 'cspm eval '3+4''  -> evaluate an expression.-  .-  * 'cspm trace spec.csp' -> interactively trace a process.-  .-  * 'cspm assert spec.csp' -> check the assertions of a specification (only some assertions are supported).-  .-  * 'cspm lts spec.csp --dotOut spec.csp.dot' -> compute the labeled transition system of a process and dump it as dot-file.-  .-  * 'cspm lts spec.csp --fdrOut spec.csp.fdr'   -> compute the LTS-    and dump it a fdr script suitable for refinement checking.-  .-  cspm is not a full featured FDR replacement.-  The main purpose of cspm is to show how the different CSPM-packages work together.-  LTS computation can demonstrate nice speed-ups on multi-core machines.-  Try for example 'cspm +RTS -N7 -RTS fdr spec.csp' to use 7 cores.   License:             BSD3-category:            Language,Formal Methods,Concurrency+category:            Language, Formal Methods, Concurrency License-File:        LICENSE-Author:              Marc Fontaine-Maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de>-cabal-Version:       >= 1.20+Author:              Marc Fontaine <Marc.Fontaine@gmx.de>+Maintainer:          Marc Fontaine <Marc.Fontaine@gmx.de>+cabal-Version:       >= 1.24 build-type:          Simple-Tested-With:         GHC == 7.8.3+Tested-With:         GHC == 8.2.1 Stability:           experimental+Extra-Source-Files:  README.md+                    ,demo/lua/cspmPrelude.lua+                    ,demo/lua/ilua.lua+                    ,demo/lua/strict.lua+                    ,demo/lua/trace.lua+                    ,include/lua/bootstrap.lua+                    ,include/lua/cspmPrelude.lua+                    ,include/lua/demo.lua+                    ,include/lua/ilua.lua+                    ,include/lua/init.lua+                    ,include/lua/strict.lua +                    +Source-Repository head+  type:     git+  location: git://github.com/MarcFontaine/cspm+ Executable cspm   Build-Depends:-    CSPM-Frontend >= 0.10 && < 0.11-    ,CSPM-CoreLanguage >= 0.3 && < 0.4-    ,CSPM-FiringRules >= 0.4 && < 0.5-    ,CSPM-Interpreter >= 0.7 && < 0.8-    ,CSPM-ToProlog >= 0.5 && < 0.6-    ,cmdargs >= 0.10.0 && < 0.11+    CSPM-Frontend >= 0.12.1 && < 0.13+    ,CSPM-CoreLanguage >= 0.3.1 && < 0.4+    ,CSPM-FiringRules >= 0.4.4 && < 0.5+    ,CSPM-Interpreter >= 0.7.1 && < 0.8+    ,CSPM-ToProlog >= 0.5.5 && < 0.6+    ,cmdargs >=0.10 && < 0.11     ,xml >= 1.3 && < 1.4     ,containers >= 0.5 && < 0.6     ,parallel >= 3.2 && < 3.3     ,base >= 4.0 && < 5.0-    ,pretty >= 1.1 && < 1.2-    ,transformers >= 0.3-    ,syb >= 0.4 && <0.5+    ,transformers >= 0.5+    ,syb >= 0.7 && <0.8     ,prettyclass >= 1.0 && < 1.1     ,hslua >=0.3.12 && <0.4    GHC-Options:-    -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans---    -funbox-strict-fields -O2 -Wall -fno-warn-orphans-    -rtsopts+    -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans -rtsopts   Default-Language: Haskell2010   Other-Extensions:     DeriveDataTypeable, StandaloneDeriving, TypeSynonymInstances, RecordWildCards@@ -82,19 +75,18 @@  Library   Build-Depends:-    CSPM-Frontend >= 0.10 && < 0.11-    ,CSPM-CoreLanguage >= 0.3 && < 0.4-    ,CSPM-FiringRules >= 0.4 && < 0.5-    ,CSPM-Interpreter >= 0.7 && < 0.8-    ,CSPM-ToProlog >= 0.5 && < 0.6-    ,cmdargs >= 0.10.0 && < 0.11+    CSPM-Frontend >= 0.12.1 && < 0.13+    ,CSPM-CoreLanguage >= 0.3.1 && < 0.4+    ,CSPM-FiringRules >= 0.4.4 && < 0.5+    ,CSPM-Interpreter >= 0.7.1 && < 0.8+    ,CSPM-ToProlog >= 0.5.5 && < 0.6+    ,cmdargs >=0.10 && < 0.11     ,xml >= 1.3 && < 1.4     ,containers >= 0.5 && < 0.6     ,parallel >= 3.2 && < 3.3     ,base >= 4.0 && < 5.0-    ,pretty >= 1.1 && < 1.2-    ,transformers >= 0.3-    ,syb >= 0.4 && <0.5+    ,transformers >= 0.5+    ,syb >= 0.7 && <0.8     ,prettyclass >= 1.0 && < 1.1     ,hslua >=0.3.12 && <0.4 

@@ -1,4 +1,4 @@-Copyright (c) Marc Fontaine 2007-2011+Copyright (c) Marc Fontaine 2007-2017  All rights reserved. 

@@ -0,0 +1,29 @@+# CSPM-cspm++This package provides the _cspm_ executable.+The _cspm_ executable serves as a command line interface to the other CSPM-packages.+It can be used to parse, translate and interpret cspm specifications and to+compute the labeled transition system (LTS) of a specification.++## Modes+_cspm_ has several modes of operation:++* 'cspm --help'      -> print a help message.+* 'cspm eval '3+4''  -> evaluate an expression.+* 'cspm trace spec.csp' -> interactively trace a process.+* 'cspm assert spec.csp' -> check the assertions of a specification (only some assertions are supported).+* 'cspm lts spec.csp --dotOut spec.csp.dot' -> compute the labeled transition system of a process and dump it as dot-file.+* 'cspm lts spec.csp --fdrOut spec.csp.fdr'   -> compute the LTS+    and dump it a fdr script suitable for refinement checking.+++## Lua Interface+_cspm_ comes with a built-in lua interpreter.++## Multi Core Support+LTS computation can demonstrate nice speed-ups on multi-core machines.+Try for example 'cspm +RTS -N7 -RTS fdr spec.csp' to use 7 cores.++## [Haddock documentation](http://hackage.haskell.org/package/CSPM-cspm)++

@@ -0,0 +1,66 @@+require 'strict'+local CSPM={}+local eval,transitions,viewProofTree,newTransistionList+local newProofTree,newValue,newProcess++function toString (o) return _cspm_toString(o) end+function valueToProcess(o) return _cspm_valueToProcess(o) end++function eval (expression, filename, verbose)+   local verb = verbose or false+   return newValue(_cspm_eval(verb, filename, expression))+end++function transitions (sigma, process)+   return newTransitionList(sigma, _cspm_transitions(sigma, process))+end++function viewProofTree (sigma, proofTree)+   local trans = _cspm_viewProofTree (proofTree)+   local res = {}+   res.event = toString (trans.event)+   res.nextState = newProcess (trans.succState, sigma)+   return res+end++function newTransitionList (sigma, rules)+   local trans = {}+   for key, rule in ipairs(rules) do+      trans[key] = newProofTree(sigma, rule)+   end+   return trans+end++function newProofTree (hsSigma, hsProof)+   local obj = viewProofTree (hsSigma, hsProof)+   obj.type = 'ProofTree'+   obj.toString = function () return toString(hsProof) end+   return obj+end++function newValue (obj)+   obj.type = 'Value'+   obj.toString = function () return toString(obj.value) end+   function obj.transitions ()+      return transitions(obj.sigma, valueToProcess(obj.value))+   end+   return obj+end++function newProcess (hsProc, hsSigma)+   local obj = {}+   obj.type  = 'Process'+   obj.toString = function () return toString(hsProc) end+   function obj.transitions ()+      return transitions(hsSigma, hsProc)+   end+   return obj+end+++CSPM.Haskell_exports_info = _cspm_exportInfo(); _cspm_exportInfo = nil+CSPM.Haskell_exports = _cspm_hsExports; _cspm_hsExports = nil+CSPM.help = "cspmPrelude for the Lua interface of CSPM"+CSPM.eval = eval++return CSPM

@@ -0,0 +1,380 @@+-- ilua.lua+-- A more friendly Lua interactive prompt+-- doesn't need '='+-- will try to print out tables recursively, subject to the pretty_print_limit value.+-- Steve Donovan, 2007+--+local pretty_print_limit = 20+local max_depth = 7+local table_clever = true+local prompt = '> '+local verbose = false+local strict = true+-- suppress strict warnings+_ = true++-- imported global functions+local sub = string.sub+local match = string.match+local find = string.find+local push = table.insert+local pop = table.remove+local append = table.insert+local concat = table.concat+local floor = math.floor+local write = io.write+local read = io.read++local savef+local collisions = {}+local G_LIB = {}+local declared = {}+local line_handler_fn, global_handler_fn+local print_handlers = {}++ilua = {}+local num_prec+local num_all++local jstack = {}++local function oprint(...)+    if savef then+        savef:write(concat({...},' '),'\n')+    end+    print(...)+end++local function join(tbl,delim,limit,depth)+    if not limit then limit = pretty_print_limit end+    if not depth then depth = max_depth end+    local n = #tbl+    local res = ''+    local k = 0+    -- very important to avoid disgracing ourselves with circular referencs...+    if #jstack > depth then+        return "..."+    end+    for i,t in ipairs(jstack) do+        if tbl == t then+            return "<self>"+        end+    end+    push(jstack,tbl)+    -- this is a hack to work out if a table is 'list-like' or 'map-like'+    -- you can switch it off with ilua.table_options {clever = false}+    local is_list+    if table_clever then+        local index1 = n > 0 and tbl[1]+        local index2 = n > 1 and tbl[2]+        is_list = index1 and index2+    end+    if is_list then+        for i,v in ipairs(tbl) do+            res = res..delim..val2str(v)+            k = k + 1+            if k > limit then+                res = res.." ... "+                break+            end+        end+    else+        for key,v in pairs(tbl) do+            if type(key) == 'number' then+                key = '['..tostring(key)..']'+            else+                key = tostring(key)+            end+            res = res..delim..key..'='..val2str(v)+            k = k + 1+            if k > limit then+                res = res.." ... "+                break+            end            +        end+    end+    pop(jstack)+    return sub(res,2)+end+++function val2str(val)+    local tp = type(val)+    if print_handlers[tp] then+        local s = print_handlers[tp](val)+        return s or '?'+    end+    if tp == 'function' then+        return tostring(val)+    elseif tp == 'table' then+        if val.__tostring  then+            return tostring(val)+        else+            return '{'..join(val,',')..'}'+        end+    elseif tp == 'string' then+        return "'"..val.."'"+    elseif tp == 'number' then+        -- we try only to apply floating-point precision for numbers deemed to be floating-point,+        -- unless the 3rd arg to precision() is true.+        if num_prec and (num_all or floor(val) ~= val) then+            return num_prec:format(val)+        else+            return tostring(val)+        end+    else+        return tostring(val)+    end+end++function _pretty_print(...)+    for i,val in ipairs(arg) do+        oprint(val2str(val))+    end+    _G['_'] = arg[1]+end++function compile(line)+    if verbose then oprint(line) end+    local f,err = loadstring(line,'local')+    return err,f+end++function evaluate(chunk)+    local ok,res = pcall(chunk)+    if not ok then+        return res+    end+    return nil -- meaning, fine!+end++function eval_lua(line)+    if savef then+        savef:write(prompt,line,'\n')+    end+    -- is the line handler interested?+    if line_handler_fn then+        line = line_handler_fn(line)+        -- returning nil here means that the handler doesn't want+        -- Lua to see the string+        if not line then return end+    end+    -- is it an expression?+    local err,chunk = compile('_pretty_print('..line..')')+    if err then+        -- otherwise, a statement?+        err,chunk = compile(line)+    end+    -- if compiled ok, then evaluate the chunk+    if not err then+        err = evaluate(chunk)+    end+    -- if there was any error, print it out+    if err then+        oprint(err)+    end+end++local function quit(code,msg)+    io.stderr:write(msg,'\n')+    os.exit(code)+end++-- functions available in scripts+function ilua.precision(len,prec,all)+    if not len then num_prec = nil+    else+        num_prec = '%'..len..'.'..prec..'f'+    end+    num_all = all+end	++function ilua.table_options(t)+    if t.limit then pretty_print_limit = t.limit end+    if t.depth then max_depth = t.depth end+    if t.clever ~= nil then table_clever = t.clever end+end++-- inject @tbl into the global namespace+function ilua.import(tbl,dont_complain,lib)+    lib = lib or '<unknown>'+    if type(tbl) == 'table' then+        for k,v in pairs(tbl) do+            local key = rawget(_G,k)+            -- NB to keep track of collisions!+            if key and k ~= '_M' and k ~= '_NAME' and k ~= '_PACKAGE' and k ~= '_VERSION' then+                append(collisions,{k,lib,G_LIB[k]})+            end+            _G[k] = v+            G_LIB[k] = lib+        end+    end+    if not dont_complain and  #collisions > 0  then+        for i, coll in ipairs(collisions) do+            local name,lib,oldlib = coll[1],coll[2],coll[3]+            write('warning: ',lib,'.',name,' overwrites ')+            if oldlib then+                write(oldlib,'.',name,'\n')+            else+                write('global ',name,'\n')+            end+        end+    end+end++function ilua.print_handler(name,handler)+    print_handlers[name] = handler+end++function ilua.line_handler(handler)+    line_handler_fn = handler+end++function ilua.global_handler(handler)+    global_handler_fn = handler+end++function ilua.print_variables()+    for name,v in pairs(declared) do+        print(name,type(_G[name]))+    end+end+--+-- strict.lua+-- checks uses of undeclared global variables+-- All global variables must be 'declared' through a regular assignment+-- (even assigning nil will do) in a main chunk before being used+-- anywhere.+--+local function set_strict()+    local mt = getmetatable(_G)+    if mt == nil then+        mt = {}+        setmetatable(_G, mt)+    end++    local function what ()+        local d = debug.getinfo(3, "S")+        return d and d.what or "C"+    end++    mt.__newindex = function (t, n, v)+        declared[n] = true+        rawset(t, n, v)+    end+      +    mt.__index = function (t, n)+        if not declared[n] and what() ~= "C" then+            local lookup = global_handler_fn and global_handler_fn(n)+            if not lookup then+                error("variable '"..n.."' is not declared", 2)+            else+                return lookup+            end+        end+        return rawget(t, n)+    end++end++--- Initial operations which may not succeed!+-- try to bring in any ilua configuration file; don't complain if this is unsuccessful+pcall(function()    +    require 'ilua-defs'+end)++-- Unix readline support, if readline.so is available...+local rl,readline,saveline+err = pcall(function()+    rl = require 'readline'  +    readline = rl.readline+    saveline = rl.add_history+end)+if not rl then+    readline = function(prompt)+        write(prompt)+        return read()+    end+    saveline = function(s) end+end++-- process command-line parameters+if arg then+    local i = 1+    +    local function parm_value(opt,parm,def)+        local val = parm:sub(3)+        if #val == 0 then+            i = i + 1+            if i > #arg then +                if not def then+                    quit(-1,"expecting parameter for option '-"..opt.."'")+                else+                    return def+                end+            end+            val = arg[i]+        end+        return val+    end+    +    while i <= #arg do+        local v = arg[i]+        local opt = v:sub(1,1)+        if opt == '-' then+            opt = v:sub(2,2)			+            if opt == 'h' then+                quit(0,"ilua (-l lib) (-L lib) (lua files)")            +            elseif opt == 'l' then+                require (parm_value(opt,v))+            elseif opt == 'L' then+                local lib = parm_value(opt,v)+                local tbl = require (lib)+                -- we cannot always trust require to return the table!+                if type(tbl) ~= 'table' then+                    tbl = _G[lib]+                end+                ilua.import(tbl,true,lib)+            elseif opt == 't' or opt == 'T' then+                local file+                if opt == 'T' then+                    file = 'ilua_'..os.date ('%y_%m_%d_%H_%M')..'.log'+                else+                    file = parm_value(opt,v,"ilua.log")+                end+                print('saving transcript "'..file..'"')+                savef = io.open(file,'w')+                savef:write('! ilua ',concat(arg,' '),'\n')+            elseif opt == 's' then+                strict = false+            elseif opt == 'v' then+                verbose = true+            end+        else -- a plain file to be executed immediately+            dofile(v)+        end+        i = i + 1+    end+end+    +print 'ILUA: Lua 5.1.2  Copyright (C) 1994-2007 Lua.org, PUC-Rio\n"quit" to end'++-- any import complaints?+ilua.import()++-- enable 'not declared' error+if strict then +    set_strict()+end++local line = readline(prompt)+while line do    +    if line == 'quit' then break end+    eval_lua(line)+    saveline(line)+    line = readline(prompt)+end++if savef then+    savef:close()+end

@@ -0,0 +1,38 @@+--+-- strict.lua+-- checks uses of undeclared global variables+-- All global variables must be 'declared' through a regular assignment+-- (even assigning nil will do) in a main chunk before being used+-- anywhere or assigned to inside a function.+--++local mt = getmetatable(_G)+if mt == nil then+  mt = {}+  setmetatable(_G, mt)+end++__STRICT = true+mt.__declared = {}++mt.__newindex = function (t, n, v)+  if __STRICT and not mt.__declared[n] then+    local w = debug.getinfo(2, "S").what+    if w ~= "main" and w ~= "C" then+      error("assign to undeclared variable '"..n.."'", 2)+    end+    mt.__declared[n] = true+  end+  rawset(t, n, v)+end++mt.__index = function (t, n)+  if not mt.__declared[n] and debug.getinfo(2, "S").what ~= "C" then+    error("variable '"..n.."' is not declared", 2)+  end+  return rawget(t, n)+end++function global(...)+   for _, v in ipairs{...} do mt.__declared[v] = true end+end

@@ -0,0 +1,50 @@+-- this is exprimental+--+require 'strict'+local CSPM = require 'cspmPrelude'++function main()+    print "start"+    test1 ()+    if #arg < 4 then return "not enough arguments" end+    test2 (arg[1],arg[2])+    print "finished"+end++function test1 ()+    print("eval an expressions ", CSPM.eval("3+3"):toString())+    print(CSPM.help)+end++function test2 (spec,entry)+    print ("Specification : ", spec)+    print ("Init          : ", entry)++    print "Loading Specification"+    local proc = CSPM.eval(entry,spec)++    print("Init-Value :", proc:toString())++    trace (10,proc)+end++function trace(maxSteps,currentState)+    for step =1, maxSteps do+        print ("Step", step, ":")+        print ("State =", currentState:toString())+        local transitions = currentState:transitions()+        if #transitions == 0 then break end+        showTransitionTable(transitions)+        currentState = transitions[1].nextState+    end+end++function showTransitionTable (transitions)+    print ("Number of Transitions :", #transitions )+    for i,trans in ipairs(transitions) do+       print ("", i, ":", trans.event)+    end+ end++test1 ()+test2 ('funBench.csp','P2')

@@ -0,0 +1,2 @@+local cspmPrelude = assert(loadstring(_cspm_prelude))+cspmPrelude()

@@ -0,0 +1,65 @@+local CSPM={}+local eval,transitions,viewProofTree,newTransistionList+local newProofTree,newValue,newProcess++function toString (o) return _cspm_toString(o) end+function valueToProcess(o) return _cspm_valueToProcess(o) end++function eval (expression, filename, verbose)+   local verb = verbose or false+   return newValue(_cspm_eval(verb, filename, expression))+end++function transitions (sigma, process)+   return newTransitionList(sigma, _cspm_transitions(sigma, process))+end++function viewProofTree (sigma, proofTree)+   local trans = _cspm_viewProofTree (proofTree)+   local res = {}+   res.event = toString (trans.event)+   res.nextState = newProcess (trans.succState, sigma)+   return res+end++function newTransitionList (sigma, rules)+   local trans = {}+   for key, rule in ipairs(rules) do+      trans[key] = newProofTree(sigma, rule)+   end+   return trans+end++function newProofTree (hsSigma, hsProof)+   local obj = viewProofTree (hsSigma, hsProof)+   obj.type = 'ProofTree'+   obj.toString = function () return toString(hsProof) end+   return obj+end++function newValue (obj)+   obj.type = 'Value'+   obj.toString = function () return toString(obj.value) end+   function obj.transitions ()+      return transitions(obj.sigma, valueToProcess(obj.value))+   end+   return obj+end++function newProcess (hsProc, hsSigma)+   local obj = {}+   obj.type  = 'Process'+   obj.toString = function () return toString(hsProc) end+   function obj.transitions ()+      return transitions(hsSigma, hsProc)+   end+   return obj+end+++CSPM.Haskell_exports_info = _cspm_exportInfo(); _cspm_exportInfo = nil+CSPM.Haskell_exports = _cspm_hsExports; _cspm_hsExports = nil+CSPM.help = "cspmPrelude for the Lua interface of CSPM"+CSPM.eval = eval++return CSPM

@@ -0,0 +1,48 @@+-- require 'strict'+-- local CSPM = require 'cspmPrelude'++function main()+    print "start"+    test1 ()+    if #arg < 4 then return "not enough arguments" end+    test2 (arg[1],arg[2])+    print "finished"+end++function test1 ()+    print(CSPM.help)+    print("eval an expressions ", CSPM.eval("3+3"):toString())+end++function test2 (spec,entry)+    print ("Specification : ", spec)+    print ("Init          : ", entry)++    print "Loading Specification"+    local proc = CSPM.eval(entry,spec)++    print("Init-Value :", proc:toString())++    trace (10,proc)+end++function trace(maxSteps,currentState)+    for step =1, maxSteps do+        print ("Step", step, ":")+        print ("State =", currentState:toString())+        local transitions = currentState:transitions()+        if #transitions == 0 then break end+        showTransitionTable(transitions)+        currentState = transitions[1].nextState+    end+end++function showTransitionTable (transitions)+    print ("Number of Transitions :", #transitions )+    for i,trans in ipairs(transitions) do+       print ("", i, ":", trans.event)+    end+ end++test1 ()+test2 ('funBench.csp','P2')

@@ -0,0 +1,380 @@+-- ilua.lua+-- A more friendly Lua interactive prompt+-- doesn't need '='+-- will try to print out tables recursively, subject to the pretty_print_limit value.+-- Steve Donovan, 2007+--+local pretty_print_limit = 20+local max_depth = 7+local table_clever = true+local prompt = '> '+local verbose = false+local strict = true+-- suppress strict warnings+_ = true++-- imported global functions+local sub = string.sub+local match = string.match+local find = string.find+local push = table.insert+local pop = table.remove+local append = table.insert+local concat = table.concat+local floor = math.floor+local write = io.write+local read = io.read++local savef+local collisions = {}+local G_LIB = {}+local declared = {}+local line_handler_fn, global_handler_fn+local print_handlers = {}++ilua = {}+local num_prec+local num_all++local jstack = {}++local function oprint(...)+    if savef then+        savef:write(concat({...},' '),'\n')+    end+    print(...)+end++local function join(tbl,delim,limit,depth)+    if not limit then limit = pretty_print_limit end+    if not depth then depth = max_depth end+    local n = #tbl+    local res = ''+    local k = 0+    -- very important to avoid disgracing ourselves with circular referencs...+    if #jstack > depth then+        return "..."+    end+    for i,t in ipairs(jstack) do+        if tbl == t then+            return "<self>"+        end+    end+    push(jstack,tbl)+    -- this is a hack to work out if a table is 'list-like' or 'map-like'+    -- you can switch it off with ilua.table_options {clever = false}+    local is_list+    if table_clever then+        local index1 = n > 0 and tbl[1]+        local index2 = n > 1 and tbl[2]+        is_list = index1 and index2+    end+    if is_list then+        for i,v in ipairs(tbl) do+            res = res..delim..val2str(v)+            k = k + 1+            if k > limit then+                res = res.." ... "+                break+            end+        end+    else+        for key,v in pairs(tbl) do+            if type(key) == 'number' then+                key = '['..tostring(key)..']'+            else+                key = tostring(key)+            end+            res = res..delim..key..'='..val2str(v)+            k = k + 1+            if k > limit then+                res = res.." ... "+                break+            end            +        end+    end+    pop(jstack)+    return sub(res,2)+end+++function val2str(val)+    local tp = type(val)+    if print_handlers[tp] then+        local s = print_handlers[tp](val)+        return s or '?'+    end+    if tp == 'function' then+        return tostring(val)+    elseif tp == 'table' then+        if val.__tostring  then+            return tostring(val)+        else+            return '{'..join(val,',')..'}'+        end+    elseif tp == 'string' then+        return "'"..val.."'"+    elseif tp == 'number' then+        -- we try only to apply floating-point precision for numbers deemed to be floating-point,+        -- unless the 3rd arg to precision() is true.+        if num_prec and (num_all or floor(val) ~= val) then+            return num_prec:format(val)+        else+            return tostring(val)+        end+    else+        return tostring(val)+    end+end++function _pretty_print(...)+    for i,val in ipairs(arg) do+        oprint(val2str(val))+    end+    _G['_'] = arg[1]+end++function compile(line)+    if verbose then oprint(line) end+    local f,err = loadstring(line,'local')+    return err,f+end++function evaluate(chunk)+    local ok,res = pcall(chunk)+    if not ok then+        return res+    end+    return nil -- meaning, fine!+end++function eval_lua(line)+    if savef then+        savef:write(prompt,line,'\n')+    end+    -- is the line handler interested?+    if line_handler_fn then+        line = line_handler_fn(line)+        -- returning nil here means that the handler doesn't want+        -- Lua to see the string+        if not line then return end+    end+    -- is it an expression?+    local err,chunk = compile('_pretty_print('..line..')')+    if err then+        -- otherwise, a statement?+        err,chunk = compile(line)+    end+    -- if compiled ok, then evaluate the chunk+    if not err then+        err = evaluate(chunk)+    end+    -- if there was any error, print it out+    if err then+        oprint(err)+    end+end++local function quit(code,msg)+    io.stderr:write(msg,'\n')+    os.exit(code)+end++-- functions available in scripts+function ilua.precision(len,prec,all)+    if not len then num_prec = nil+    else+        num_prec = '%'..len..'.'..prec..'f'+    end+    num_all = all+end	++function ilua.table_options(t)+    if t.limit then pretty_print_limit = t.limit end+    if t.depth then max_depth = t.depth end+    if t.clever ~= nil then table_clever = t.clever end+end++-- inject @tbl into the global namespace+function ilua.import(tbl,dont_complain,lib)+    lib = lib or '<unknown>'+    if type(tbl) == 'table' then+        for k,v in pairs(tbl) do+            local key = rawget(_G,k)+            -- NB to keep track of collisions!+            if key and k ~= '_M' and k ~= '_NAME' and k ~= '_PACKAGE' and k ~= '_VERSION' then+                append(collisions,{k,lib,G_LIB[k]})+            end+            _G[k] = v+            G_LIB[k] = lib+        end+    end+    if not dont_complain and  #collisions > 0  then+        for i, coll in ipairs(collisions) do+            local name,lib,oldlib = coll[1],coll[2],coll[3]+            write('warning: ',lib,'.',name,' overwrites ')+            if oldlib then+                write(oldlib,'.',name,'\n')+            else+                write('global ',name,'\n')+            end+        end+    end+end++function ilua.print_handler(name,handler)+    print_handlers[name] = handler+end++function ilua.line_handler(handler)+    line_handler_fn = handler+end++function ilua.global_handler(handler)+    global_handler_fn = handler+end++function ilua.print_variables()+    for name,v in pairs(declared) do+        print(name,type(_G[name]))+    end+end+--+-- strict.lua+-- checks uses of undeclared global variables+-- All global variables must be 'declared' through a regular assignment+-- (even assigning nil will do) in a main chunk before being used+-- anywhere.+--+local function set_strict()+    local mt = getmetatable(_G)+    if mt == nil then+        mt = {}+        setmetatable(_G, mt)+    end++    local function what ()+        local d = debug.getinfo(3, "S")+        return d and d.what or "C"+    end++    mt.__newindex = function (t, n, v)+        declared[n] = true+        rawset(t, n, v)+    end+      +    mt.__index = function (t, n)+        if not declared[n] and what() ~= "C" then+            local lookup = global_handler_fn and global_handler_fn(n)+            if not lookup then+                error("variable '"..n.."' is not declared", 2)+            else+                return lookup+            end+        end+        return rawget(t, n)+    end++end++--- Initial operations which may not succeed!+-- try to bring in any ilua configuration file; don't complain if this is unsuccessful+pcall(function()    +    require 'ilua-defs'+end)++-- Unix readline support, if readline.so is available...+local rl,readline,saveline+err = pcall(function()+    rl = require 'readline'  +    readline = rl.readline+    saveline = rl.add_history+end)+if not rl then+    readline = function(prompt)+        write(prompt)+        return read()+    end+    saveline = function(s) end+end++-- process command-line parameters+if arg then+    local i = 1+    +    local function parm_value(opt,parm,def)+        local val = parm:sub(3)+        if #val == 0 then+            i = i + 1+            if i > #arg then +                if not def then+                    quit(-1,"expecting parameter for option '-"..opt.."'")+                else+                    return def+                end+            end+            val = arg[i]+        end+        return val+    end+    +    while i <= #arg do+        local v = arg[i]+        local opt = v:sub(1,1)+        if opt == '-' then+            opt = v:sub(2,2)			+            if opt == 'h' then+                quit(0,"ilua (-l lib) (-L lib) (lua files)")            +            elseif opt == 'l' then+                require (parm_value(opt,v))+            elseif opt == 'L' then+                local lib = parm_value(opt,v)+                local tbl = require (lib)+                -- we cannot always trust require to return the table!+                if type(tbl) ~= 'table' then+                    tbl = _G[lib]+                end+                ilua.import(tbl,true,lib)+            elseif opt == 't' or opt == 'T' then+                local file+                if opt == 'T' then+                    file = 'ilua_'..os.date ('%y_%m_%d_%H_%M')..'.log'+                else+                    file = parm_value(opt,v,"ilua.log")+                end+                print('saving transcript "'..file..'"')+                savef = io.open(file,'w')+                savef:write('! ilua ',concat(arg,' '),'\n')+            elseif opt == 's' then+                strict = false+            elseif opt == 'v' then+                verbose = true+            end+        else -- a plain file to be executed immediately+            dofile(v)+        end+        i = i + 1+    end+end+    +print 'ILUA: Lua 5.1.2  Copyright (C) 1994-2007 Lua.org, PUC-Rio\n"quit" to end'++-- any import complaints?+ilua.import()++-- enable 'not declared' error+if strict then +    set_strict()+end++local line = readline(prompt)+while line do    +    if line == 'quit' then break end+    eval_lua(line)+    saveline(line)+    line = readline(prompt)+end++if savef then+    savef:close()+end

@@ -0,0 +1,3 @@+print ("initializing lua embedding")+local cspmPrelude = assert(loadstring(_cspm_cspmPrelude()))+CSPM=cspmPrelude()

@@ -0,0 +1,38 @@+--+-- strict.lua+-- checks uses of undeclared global variables+-- All global variables must be 'declared' through a regular assignment+-- (even assigning nil will do) in a main chunk before being used+-- anywhere or assigned to inside a function.+--++local mt = getmetatable(_G)+if mt == nil then+  mt = {}+  setmetatable(_G, mt)+end++__STRICT = true+mt.__declared = {}++mt.__newindex = function (t, n, v)+  if __STRICT and not mt.__declared[n] then+    local w = debug.getinfo(2, "S").what+    if w ~= "main" and w ~= "C" then+      error("assign to undeclared variable '"..n.."'", 2)+    end+    mt.__declared[n] = true+  end+  rawset(t, n, v)+end++mt.__index = function (t, n)+  if not mt.__declared[n] and debug.getinfo(2, "S").what ~= "C" then+    error("variable '"..n.."' is not declared", 2)+  end+  return rawget(t, n)+end++function global(...)+   for _, v in ipairs{...} do mt.__declared[v] = true end+end

@@ -1,15 +1,14 @@ ---------------------------------------------------------------------------- -- | -- Module      :  CSPM.LTS.LTS--- Copyright   :  (c) Fontaine 2009 - 2011+-- Copyright   :  (c) Fontaine 2009 - 2017 -- License     :  BSD3 --  -- Maintainer  :  Fontaine@cs.uni-duesseldorf.de -- Stability   :  experimental -- Portability :  GHC-only ---{-# LANGUAGE BangPatterns #-}-{-# Language DeriveDataTypeable #-}+{-# LANGUAGE BangPatterns, DeriveDataTypeable,FlexibleContexts,RankNTypes  #-}  module CSPM.LTS.LTS where@@ -53,7 +52,8 @@     hashTrans :: Rule INT -> Interpreter.Digest     hashTrans r = let (from,trans,to) = viewRule r       in mix3 (hash from) (hashEvent trans) (hash to)-+    hashEvent ::+      forall i. Hash (CSPM.CoreLanguage.Event.Event i) => TTE i -> Digest     hashEvent e = case e of       TickEvent -> hs "tickEvent"       TauEvent  -> hs "tauEvent"

@@ -1,7 +1,14 @@ ---------------------------------------------------------------------------- -- | -- Module      :  Scripting.LuaUtils+-- Copyright   :  (c) Fontaine 2009 - 2017+-- License     :  BSD3+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only --+-- -- Utility function for Lua Scripting ---------------------------------------------------------------------------- {-# Language DeriveDataTypeable #-}@@ -16,6 +23,7 @@  import Control.Monad import Data.Dynamic+import Data.Typeable (typeOf) import Foreign.StablePtr import Foreign.Ptr import Foreign.C