diff --git a/CSPM-cspm.cabal b/CSPM-cspm.cabal --- a/CSPM-cspm.cabal +++ b/CSPM-cspm.cabal @@ -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 -cabal-Version: >= 1.20 +Author: Marc Fontaine +Maintainer: Marc Fontaine +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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) Marc Fontaine 2007-2011 +Copyright (c) Marc Fontaine 2007-2017 All rights reserved. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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) + + diff --git a/demo/lua/cspmPrelude.lua b/demo/lua/cspmPrelude.lua new file mode 100644 --- /dev/null +++ b/demo/lua/cspmPrelude.lua @@ -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 diff --git a/demo/lua/ilua.lua b/demo/lua/ilua.lua new file mode 100644 --- /dev/null +++ b/demo/lua/ilua.lua @@ -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 "" + 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 '' + 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 diff --git a/demo/lua/strict.lua b/demo/lua/strict.lua new file mode 100644 --- /dev/null +++ b/demo/lua/strict.lua @@ -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 diff --git a/demo/lua/trace.lua b/demo/lua/trace.lua new file mode 100644 --- /dev/null +++ b/demo/lua/trace.lua @@ -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') diff --git a/include/lua/bootstrap.lua b/include/lua/bootstrap.lua new file mode 100644 --- /dev/null +++ b/include/lua/bootstrap.lua @@ -0,0 +1,2 @@ +local cspmPrelude = assert(loadstring(_cspm_prelude)) +cspmPrelude() diff --git a/include/lua/cspmPrelude.lua b/include/lua/cspmPrelude.lua new file mode 100644 --- /dev/null +++ b/include/lua/cspmPrelude.lua @@ -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 diff --git a/include/lua/demo.lua b/include/lua/demo.lua new file mode 100644 --- /dev/null +++ b/include/lua/demo.lua @@ -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') diff --git a/include/lua/ilua.lua b/include/lua/ilua.lua new file mode 100644 --- /dev/null +++ b/include/lua/ilua.lua @@ -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 "" + 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 '' + 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 diff --git a/include/lua/init.lua b/include/lua/init.lua new file mode 100644 --- /dev/null +++ b/include/lua/init.lua @@ -0,0 +1,3 @@ +print ("initializing lua embedding") +local cspmPrelude = assert(loadstring(_cspm_cspmPrelude())) +CSPM=cspmPrelude() diff --git a/include/lua/strict.lua b/include/lua/strict.lua new file mode 100644 --- /dev/null +++ b/include/lua/strict.lua @@ -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 diff --git a/src/CSPM/LTS/LTS.hs b/src/CSPM/LTS/LTS.hs --- a/src/CSPM/LTS/LTS.hs +++ b/src/CSPM/LTS/LTS.hs @@ -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" diff --git a/src/Scripting/LuaUtils.hs b/src/Scripting/LuaUtils.hs --- a/src/Scripting/LuaUtils.hs +++ b/src/Scripting/LuaUtils.hs @@ -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