Skip to content

Allow CSE optimization to cross between future and past time #25

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

Open
aaurandt opened this issue Apr 7, 2025 · 0 comments
Open

Allow CSE optimization to cross between future and past time #25

aaurandt opened this issue Apr 7, 2025 · 0 comments
Labels

Comments

@aaurandt
Copy link
Contributor

aaurandt commented Apr 7, 2025

Currently, past and future time specs are kept completely separate within C2PO. This means the even simple instructions like loading an atomic are duplicated for both future and past time.

One possible solution would be to

  • Have C2PO still check for mixed time formulas in type_check.py to prohibit users from creating these formulas
  • Have past and future specifications be represented as a single data structure in the rest of C2PO to allow for CSE to apply to both
@aaurandt aaurandt added the c2po label Apr 7, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant