K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi,

I can see two problems here:

1) you're using " " instead of ' ', so the shell tries to translate what you have inside the quotes - ~ is shorthand for home directory, so it tries to find a file ~Ltl, i.e., the home directory of user Ltl (which doesn't exist)

2) there's a space between Ltl and  __error - doubt that there should be one.

So maybe try this:

LTLMC='[]Ltl ~Ltl__error' ./bad

Note - have not looked into this myself, so have no idea if "[]Ltl" is correct or not. Posting to the list as well, in case someone with more experience can help out (and possibly correct the README.md file if it's wrong).

Cheers,

Christos

On 15/03/2018 09:43, 璟临天下 wrote:

hello 

i have handled the non-determinism problem by changing the range of non-deterministic operation. Now i want to do something about LTL model checking. and i read c-semantics/examples/README.md, but got the error message like below:

what causes this problem? do i miss something?

dexter@dexter-virtual-machine:~/Desktop/C2/c-semantics-3.4.0/examples/ltlmc$ kcc -s bad.c -o bad

dexter@dexter-virtual-machine:~/Desktop/C2/c-semantics-3.4.0/examples/ltlmc$ LTLMC="[]Ltl ~Ltl __error" ./bad

LTL model checking... (with non-deterministic _expression_ sequencing)

[Error] Critical: Cannot retrieve file content. Make sure that file: ~Ltl

exists.

File: internal

Location: FileUtil.java