Documentation

[mbuit82]

Hey Ben, I've been taking a look at the refactoring and it looks great! I like the idea of a StateSpace object. (I made a new issue because I didn't want to clutter the old Data Structure issue) I've been adding documentation and comments here and there, and there's a couple things I'd let you know:

1. I renamed make_constraints to define_N_semantics. My reasoning was that make_constraints doesn't actually make the constraints, it makes the function that makes the constraints (something that was even in the docstring for the function lol). So I gave it that other name—if you think of something else feel free to change it, but just thought that change may help things be more clear.
2. Some of my comments have been with an eye towards using the package in a python file (like you'd use numpy or z3 or any other package in a file). Is that something you still think is worth pursuing?
3. I had a small issue with the names of the imports in model_structure. Is there a reason they were model_checker.____ as opposed to just being ____?

[benbrastmckie]

I think define_N_semantics is a much better name, and yes, I think using the package in a python file is definitely the direction forward. Parallel to that I have been thinking about adding a flag to get it to generate a local semantics module that could be easily adapted and used to override the built in semantics. But these are totally independent and I think useful in quite different ways. The latter is more for development and adding new operators, whereas being able to import the package and its functions is better for applications and really studying the logic that results.

As for the imports, I added the full path in order to easily build the package for uploading to PyPI. I added the following to __main__.py so that Python can find the module paths as stated:

# Get the directory path of the current file
current_dir = os.path.dirname(__file__)
# Construct the full path to your project root
project_root = os.path.abspath(os.path.join(current_dir, ".."))
# Add the project root to the Python path
sys.path.append(project_root)

If that doesn't work, you might try experimenting to get Python find the right path to the modules.

[mbuit82]

Sounds good! I think I fixed the issue by adding project_root = project_root[:-4] # bandaid fix to remove "/src" from the root to that code before appending project_root to sys.path. Basically before whenever you'd type model_checker.xyz it'd still import from the package downloaded (I could tell because it would find the function make_constraints even though that's no longer in the project, only in the published package). Doing some digging it seems to be because the first place python checks when doing imports is the packages you've downloaded, then it seems to check locally. So I made project_root to end with Code by removing /src and changing the paths to src.model_checker.xyz to unambiguously identify for python the module as the one in the project, not the downloaded package. It's a bit of a bandaid fix so there's probably a more technical way to do it but this seems to work

[benbrastmckie]

Seems to be working great!

[mbuit82]

Ran into an issue trying to use the package with the src. addition I had put in—basically it now wouldn't find src in the downloaded package, so I added it back. Since the reason to add src. was to make quick tests easier, but it is an issue we need to keep in mind—I'm not sure how to force it to read the local folder instead of first checking dowloaded packages though I'm sure there's a way to do this for editing, and then whenever things are pushed to turn it off. For now I've taken src. away from all the paths in the imports, and it seems to be working well as a package so to speak (just needs to be published to PyPi to confirm)

[benbrastmckie]

I was able to build the package successfully. I haven't tried uploading it to PyPI just yet but assume that wouldn't present any further issue. But I'll look out for that on the next upload.