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.

Sign up for GitHub

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

Jump to bottom

Jupiter: Adding History Variable #37

Open
hengxin opened this issue Dec 15, 2018 · 0 comments
Open

Jupiter: Adding History Variable #37

hengxin opened this issue Dec 15, 2018 · 0 comments
Assignees
@hengxin @tangruize
Labels
model check to model check priority:normal with normal priority question refactor refactor code/file todo TODO
Projects
Wei-Jupiter-TLA

Comments

@hengxin
Copy link
Owner

hengxin commented Dec 15, 2018 •
edited
Loading

Jupiter: Adding History Variable

Reference:

Possible Solution: (In branch: Jupiter-History)

  • Create JupiterH module, which contains the history variable list and the history collecting procedure
  • Let xxJupiterH extends/instance JupiterH (Instance Level Error)
@hengxin hengxin added question refactor refactor code/file model check to model check todo TODO labels Dec 15, 2018
@hengxin hengxin self-assigned this Dec 15, 2018
@hengxin hengxin added this to To do in Wei-Jupiter-TLA via automation Dec 15, 2018
@hengxin hengxin added the priority:low with low priority label Jan 1, 2019
hengxin pushed a commit that referenced this issue Jan 1, 2019
Wei-jupiter-tla: +JupiterH for introducing history variable; +AbsJupi…
f90190e 
…terH for test (not passed); see Issue #37
@hengxin hengxin pinned this issue Jan 1, 2019
@hengxin hengxin added priority:normal with normal priority and removed priority:low with low priority labels Jan 1, 2019
@hengxin hengxin unpinned this issue Feb 1, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@hengxin hengxin

@tangruize tangruize

Labels
model check to model check priority:normal with normal priority question refactor refactor code/file todo TODO
Projects
Wei-Jupiter-TLA
  
To do
Milestone
No milestone
Development

No branches or pull requests
2 participants
@hengxin @tangruize