hengxin/tlaplus-at-nju-disalg issues and pull requests

#52 - + fix absolute path Makefile

Pull Request - State: closed - Opened by tangruize almost 6 years ago

#52 - + fix absolute path Makefile

Pull Request - State: closed - Opened by tangruize almost 6 years ago

#51 - + TLAPS for Peterson algorithm

Pull Request - State: closed - Opened by Starydark almost 6 years ago

#51 - + TLAPS for Peterson algorithm

Pull Request - State: closed - Opened by Starydark almost 6 years ago

#50 - CSComm: Refactor

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, todo, priority:normal

#50 - CSComm: Refactor

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, todo, priority:normal

#49 - Jupiter: Code Formatting

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, todo, priority:low, formatting

#49 - Jupiter: Code Formatting

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, todo, priority:low, formatting

#48 - JupiterInterface: Integrate the C/S Interaction (i.e., Communication) in JupiterInterface

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: question, refactor, model check, Rearrangement, todo, priority:normal

#48 - JupiterInterface: Integrate the C/S Interaction (i.e., Communication) in JupiterInterface

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: question, refactor, model check, Rearrangement, todo, priority:normal

#47 - JupiterInterface: How to Modify `state` in the Interface Level?

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:normal

#47 - JupiterInterface: How to Modify `state` in the Interface Level?

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:normal

#46 - OP, OpOperators, OT: Refactor

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:low

#46 - OP, OpOperators, OT: Refactor

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:low

#45 - Jupiter: Refactor `Do(c)`

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo

#45 - Jupiter: Refactor `Do(c)`

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo

#44 - AJupiter Family: AJupiter, AJupiterExtended, AJupiterImplXJupiter

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:high

#44 - AJupiter Family: AJupiter, AJupiterExtended, AJupiterImplXJupiter

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:high

#43 - AJupiterImplXJupiter

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: model check, todo, priority:high

#43 - AJupiterImplXJupiter

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: model check, todo, priority:high

#42 - TLAPS seminar examples and slide.

Pull Request - State: closed - Opened by tangruize almost 6 years ago

#42 - TLAPS seminar examples and slide.

Pull Request - State: closed - Opened by tangruize almost 6 years ago

#41 - AJupiter: Check the Correctness of AJupiter

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: bug, question, todo, priority:high

#41 - AJupiter: Check the Correctness of AJupiter

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: bug, question, todo, priority:high

#40 - + RGA & OT function

Pull Request - State: closed - Opened by JYwellin almost 6 years ago

#40 - + RGA & OT function

Pull Request - State: closed - Opened by JYwellin almost 6 years ago

#39 - Jupiter: Refinement Structure

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: question, refactor, performance, todo

#39 - Jupiter: Refinement Structure

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: question, refactor, performance, todo

#38 - Jupiter: Specification

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:low

#38 - Jupiter: Specification

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: refactor, model check, Rearrangement, todo, priority:low

#37 - Jupiter: Adding History Variable

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: question, refactor, model check, todo, priority:normal

#37 - Jupiter: Adding History Variable

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: question, refactor, model check, todo, priority:normal

#36 - AbsJupiter

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: model check, todo

#36 - AbsJupiter

Issue - State: closed - Opened by hengxin almost 6 years ago
Labels: model check, todo

#35 - Wei-jupiter-tla Project: wiki

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: Rearrangement, documentation

#35 - Wei-jupiter-tla Project: wiki

Issue - State: open - Opened by hengxin almost 6 years ago
Labels: Rearrangement, documentation

#34 - Jupiter: xForm

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check, performance, todo, priority:high

#34 - Jupiter: xForm

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check, performance, todo, priority:high

#33 - Wei-jupiter-tla Project: Basic Code/File Refactor

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, model check, Rearrangement

#33 - Wei-jupiter-tla Project: Basic Code/File Refactor

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, model check, Rearrangement

#32 - XJupiter, XJupiterImplCJupiter: Replace 'seq' by 'set' in xForm

Issue - State: closed - Opened by hengxin about 6 years ago - 1 comment
Labels: refactor, model check

#32 - XJupiter, XJupiterImplCJupiter: Replace 'seq' by 'set' in xForm

Issue - State: closed - Opened by hengxin about 6 years ago - 1 comment
Labels: refactor, model check

#31 - CJupiter, XJupiter, XJupiterExtended, XJupiterImplCJupiter: Performance Issues

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, performance

#31 - CJupiter, XJupiter, XJupiterExtended, XJupiterImplCJupiter: Performance Issues

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, performance

#30 - XJupiterImplCJupiter: Symmetry Sets in Models

Issue - State: open - Opened by hengxin about 6 years ago
Labels: question, performance

#30 - XJupiterImplCJupiter: Symmetry Sets in Models

Issue - State: open - Opened by hengxin about 6 years ago
Labels: question, performance

#29 - Rename `AdditionalxxxOperators` Files to xxxUtils

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor

#29 - Rename `AdditionalxxxOperators` Files to xxxUtils

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor

#28 - XJupiterExtended: Extend `XJupiter` by Really `EXTENDS` It

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#28 - XJupiterExtended: Extend `XJupiter` by Really `EXTENDS` It

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#27 - + prophecy variables

Pull Request - State: closed - Opened by Starydark about 6 years ago

#27 - + prophecy variables

Pull Request - State: closed - Opened by Starydark about 6 years ago

#26 - Add slice ACX_Jupiter.pptx and some improvement

Pull Request - State: closed - Opened by tangruize about 6 years ago - 2 comments

#26 - Add slice ACX_Jupiter.pptx and some improvement

Pull Request - State: closed - Opened by tangruize about 6 years ago - 2 comments

#25 - CJupiter and XJupter: State Space Data Structure

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: question, refactor, model check, todo

#25 - CJupiter and XJupter: State Space Data Structure

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: question, refactor, model check, todo

#24 - Jupiter: To Separate Common Interfaces from Implementations

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#24 - Jupiter: To Separate Common Interfaces from Implementations

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#23 - CJupiter&XJupiter: `ds` is redundant

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, model check

#23 - CJupiter&XJupiter: `ds` is redundant

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor, model check

#22 - CJupiter: Replacing `sctx` and `soids` with `serial`

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#22 - CJupiter: Replacing `sctx` and `soids` with `serial`

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#21 - XJupiterImplCJupiter: the `css` part of the refinement mapping is wrong

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: bug, model check

#21 - XJupiterImplCJupiter: the `css` part of the refinement mapping is wrong

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: bug, model check

#20 - Jupiter: fairness requirements

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: bug, model check

#20 - Jupiter: fairness requirements

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: bug, model check

#19 - XJupiter: `ccur[c \in Client]` and `scur[c \in Client]` can be combined into one: `cur[r \in Replica]`

Issue - State: closed - Opened by hengxin about 6 years ago
Labels: refactor, model check

#18 - Jupiter: Each client is responsible for ignoring the messages/operations generated by itself

Issue - State: open - Opened by hengxin about 6 years ago
Labels: refactor

#17 - + TLC Model Checker

Pull Request - State: closed - Opened by Starydark about 6 years ago

#16 - + history variables slice.

Pull Request - State: closed - Opened by tangruize about 6 years ago

#15 - add StateCounter.tla with bugs for checking EC

Pull Request - State: closed - Opened by zfwang96 over 6 years ago

#14 - Merge pull request #3 from Disalg-ICS-NJU/master

Pull Request - State: closed - Opened by zfwang96 over 6 years ago

#13 - + Refinement

Pull Request - State: closed - Opened by JYwellin over 6 years ago

#12 - +HowAWSUsesFormalMethods

Pull Request - State: closed - Opened by Starydark over 6 years ago

#11 - + tla and pdf file

Pull Request - State: closed - Opened by tangruize over 6 years ago

#10 - + The Alternating Bit Protocol slide.

Pull Request - State: closed - Opened by tangruize over 6 years ago

#9 - +PaxosStore

Pull Request - State: closed - Opened by Starydark over 6 years ago - 1 comment

#8 - + Implementation slides.

Pull Request - State: closed - Opened by zfwang96 over 6 years ago

#7 - + OT

Pull Request - State: closed - Opened by JYwellin over 6 years ago

#6 - + paxos

Pull Request - State: closed - Opened by Starydark over 6 years ago

#5 - + SetEuclid & OT design

Pull Request - State: closed - Opened by JYwellin over 6 years ago

#4 - + Two-Phase Commit slides.

Pull Request - State: closed - Opened by zfwang96 over 6 years ago

#3 - + Generalized DieHard Problem Sildes

Pull Request - State: closed - Opened by Starydark over 6 years ago

#2 - + Euclid slides.

Pull Request - State: closed - Opened by zfwang96 over 6 years ago

#1 - + DieHard & TCommit slides.

Pull Request - State: closed - Opened by tangruize over 6 years ago

GitHub / hengxin/tlaplus-at-nju-disalg issues and pull requests