Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prism-auto unable to run PRISM? #5

Open
xhajnal opened this issue Oct 22, 2020 · 1 comment
Open

Prism-auto unable to run PRISM? #5

xhajnal opened this issue Oct 22, 2020 · 1 comment

Comments

@xhajnal
Copy link

xhajnal commented Oct 22, 2020

I was trying to run the PRISM benchmark as provided here: http://www.prismmodelchecker.org/benchmarks/

matej@Skadi:~/Git$ git clone https://github.com/prismmodelchecker/prism-benchmarks
matej@Skadi:~/Git$ export PATH="/home/matej/prism-4.5-linux64/etc/scripts:$PATH"

unfortunately, my PRISM 4.5 running on Ubuntu 18 replied:

matej@Skadi:~/Git$ prism-auto prism-benchmarks/models/dtmcs --filter-models "states<10000" --args-list "-pow,-jac,-gs" --log logs --log-subdir
Usage: prism-auto [options] args

prism-auto: error: no such option: --filter-models

Followed this, I have tried to replace the prism-auto with the linked prism-auto file(https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-auto)

matej@Skadi:~/Git$ prism-auto prism-benchmarks/models/dtmcs --log logs --log-subdir
prism prism-benchmarks/models/dtmcs/brp/brp.pm -const N=16,MAX=2 prism-benchmarks/models/dtmcs/brp/p1.pctl
Traceback (most recent call last):
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 1180, in <module>
    benchmarkDir(arg)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 929, in benchmarkDir
    benchmarkDir(os.path.join(dir, file))
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 933, in benchmarkDir
    benchmarkModelFile(modelFile[0], modelFile[1], dir)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 987, in benchmarkModelFile
    benchmark(modelFile, modelArgs + args + [propertiesFile] + argsp, dir)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 901, in benchmark
    runPrism(modelFileArg + args, [], dir)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 627, in runPrism
    exitCode = execute(prismArgs)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto", line 727, in execute
    proc = subprocess.Popen(args)
  File "/home/matej/.pyenv/versions/3.8.1/lib/python3.8/subprocess.py", line 854, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "/home/matej/.pyenv/versions/3.8.1/lib/python3.8/subprocess.py", line 1702, in _execute_child
    raise child_exception_type(errno_num, err_msg, err_filename)
FileNotFoundError: [Errno 2] No such file or directory: 'prism'

although my command line prism works fine:

matej@Skadi:~/Git$ prism --version
PRISM version 4.5

trying to run as root results in a different error (rename the downloaded script to prism-auto3)

root@Skadi:/home/matej/Git# prism-auto3 prism-benchmarks/models/dtmcs --filter-models "states<10000" --args-list "-pow,-jac,-gs" --log logs --log-subdir
Traceback (most recent call last):
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto3", line 1180, in <module>
    benchmarkDir(arg)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto3", line 929, in benchmarkDir
    benchmarkDir(os.path.join(dir, file))
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto3", line 931, in benchmarkDir
    modelFiles = getModelsInDir(dir)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto3", line 149, in getModelsInDir
    modelFiles = filterModels(modelFiles, options.filterModels, dir)
  File "/home/matej/prism-4.5-linux64/etc/scripts/prism-auto3", line 166, in filterModels
    with open(os.path.join(dir, options.modelsInfoFilename), newline='') as csvfile:
TypeError: 'newline' is an invalid keyword argument for this function

Thank you.

@davexparker
Copy link
Member

Hi @xhajnal. The --filter-models switch was added to prism-auto after the 4.5 release. But it should be possible to directly run the newest version of prism-auto, linking to an older version of PRISM, as you are attempting. For the middle failure above (No such file or directory: 'prism'), it looks like prism-auto is not finding prism in your path. Try specifying the location by passing to prism-auto the switch -p /full/path/to/prism/bin/prism.

(Not sure about the issue when running as root, but that should not be necessary)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants