eth-sri / psi Goto Github PK

Dear PSI team,

Thanks for the nice solver and clean documentation.

It would be very useful if we can specify an option so that the solver produces parameters of the posterior distribution as well as the density function. For example, when the posterior distribution is a normal, then it would be more useful if we could just get the mean and standard deviation (possibly in the csv form).
I read the github page and the CAV 2016 paper, but I couldn't figure out how to do it. So now I think that the current solver does not have the functionality.

Do you also think it is a good thing to do?

Thanks,
Gwonsoo

I was only able to compile the code with the DMD compiler up to version v2.078.3. Later version did not work.

The python package pyd, which allows for interoperability between D-Lang and python does also have a module named util. This causes pyd to complain about psi having likewise a file named util.

Renaming util to dutil (or anything else) resolves this issues and does not require any more to run a renaming script prior to writing a wrapper for psi in python using pyd.

I am learning psi. I found a small problem.
Assume two DExprs a and b have the same guard, such as [x>0]. if we do the div operation a/b and simplify the distribution, the guard will be eliminated. I think it is not right.

The example given in the README is expecting prelude.psi to be available.
I expect prelude.psi to be packed with the binary or being available in shared for psi to find prelude. This needs to be documented as it is not obivious.

$ cat example.psi 
def main(){
    a := gauss(0,1);
    b := gauss(0,1);
    return if a > b { a } else { b };
}
$ ~/bin/psi example.psi 
error: prelude.psi: no such file

I tried to compile the new-types branch since it's newer than the master branch and contains some very interesting examples. But running the program dependencies-release.sh fails with errors about submodules that are not public available: github.com:tgehr/ast.git and github.com:tgehr/util.git. Here's the errors:

Cloning into '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/ast'...
Warning: Permanently added the RSA host key for IP address '140.82.114.3' to the list of known hosts.
[email protected]: Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
fatal: clone of '[email protected]:tgehr/ast.git' into submodule path '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/ast' failed
Failed to clone 'ast'. Retry scheduled
Cloning into '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/util'...
[email protected]: Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
fatal: clone of '[email protected]:tgehr/util.git' into submodule path '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/util' failed
Failed to clone 'util'. Retry scheduled
Cloning into '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/ast'...
[email protected]: Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
fatal: clone of '[email protected]:tgehr/ast.git' into submodule path '/home/hakank/probabilistic_programming/psi/psi_new_types/psi/ast' failed
Failed to clone 'ast' a second time, aborting

Would it be possible to make these repos public available?

Best,

Hakan

./build-release.sh: line 18: ldmd2: command not found
./build-release.sh: line 21: ldmd2: command not found

Need to add commands for unzipping ldc2-1.32.0-osx-x86_64.tar.xz