-
Notifications
You must be signed in to change notification settings - Fork 202
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Added gitattributes file * Unified all line endings to LF Signed-off-by: Andrew Helwer <[email protected]>
- Loading branch information
Showing
141 changed files
with
13,124 additions
and
13,122 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| * text=auto | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
Binary file not shown.
Large diffs are not rendered by default.
Oops, something went wrong.
Binary file not shown.
Large diffs are not rendered by default.
Oops, something went wrong.
58 changes: 29 additions & 29 deletions
58
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/.project
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,29 +1,29 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>CarTalkPuzzle</name> | ||
| <comment></comment> | ||
| <projects> | ||
| </projects> | ||
| <buildSpec> | ||
| <buildCommand> | ||
| <name>toolbox.builder.TLAParserBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| <buildCommand> | ||
| <name>toolbox.builder.PCalAlgorithmSearchingBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| </buildSpec> | ||
| <natures> | ||
| <nature>toolbox.natures.TLANature</nature> | ||
| </natures> | ||
| <linkedResources> | ||
| <link> | ||
| <name>CarTalkPuzzle.tla</name> | ||
| <type>1</type> | ||
| <location>C:/lamport/tla/newtools/tla-workspace/examples/CarTalkPuzzle/CarTalkPuzzle.tla</location> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <projectDescription> | ||
| <name>CarTalkPuzzle</name> | ||
| <comment></comment> | ||
| <projects> | ||
| </projects> | ||
| <buildSpec> | ||
| <buildCommand> | ||
| <name>toolbox.builder.TLAParserBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| <buildCommand> | ||
| <name>toolbox.builder.PCalAlgorithmSearchingBuilder</name> | ||
| <arguments> | ||
| </arguments> | ||
| </buildCommand> | ||
| </buildSpec> | ||
| <natures> | ||
| <nature>toolbox.natures.TLANature</nature> | ||
| </natures> | ||
| <linkedResources> | ||
| <link> | ||
| <name>CarTalkPuzzle.tla</name> | ||
| <type>1</type> | ||
| <location>C:/lamport/tla/newtools/tla-workspace/examples/CarTalkPuzzle/CarTalkPuzzle.tla</location> | ||
| </link> | ||
| </linkedResources> | ||
| </projectDescription> |
8 changes: 4 additions & 4 deletions
8
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/.settings/org.lamport.tla.toolbox.prefs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,4 +1,4 @@ | ||
| #Wed Mar 13 11:12:12 PDT 2013 | ||
| ProjectRootFile=C\:\\lamport\\tla\\newtools\\tla-workspace\\examples\\CarTalkPuzzle\\CarTalkPuzzle.tla | ||
| ProjectToolboxDirSize=396 | ||
| eclipse.preferences.version=1 | ||
| #Wed Mar 13 11:12:12 PDT 2013 | ||
| ProjectRootFile=C\:\\lamport\\tla\\newtools\\tla-workspace\\examples\\CarTalkPuzzle\\CarTalkPuzzle.tla | ||
| ProjectToolboxDirSize=396 | ||
| eclipse.preferences.version=1 |
2 changes: 1 addition & 1 deletion
2
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle.aux
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1 +1 @@ | ||
| \relax | ||
| \relax |
Binary file modified
BIN
-3 Bytes
(100%)
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle.pdf
Binary file not shown.
76 changes: 38 additions & 38 deletions
76
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle___Model_1.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,38 +1,38 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_1"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="\* ExpandSolutions \* CHOOSE B \in Break : IsSolution(B) <<3^5 - 1, 40 + 3^4>>"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;40;0;0"/> | ||
| <listEntry value="P;;4;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_1"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="\* ExpandSolutions \* CHOOSE B \in Break : IsSolution(B) <<3^5 - 1, 40 + 3^4>>"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;40;0;0"/> | ||
| <listEntry value="P;;4;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> |
76 changes: 38 additions & 38 deletions
76
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle___Model_2.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,38 +1,38 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_2"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="AllSolutions"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;15;0;0"/> | ||
| <listEntry value="P;;4;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_2"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="AllSolutions"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;15;0;0"/> | ||
| <listEntry value="P;;4;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> |
76 changes: 38 additions & 38 deletions
76
specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/CarTalkPuzzle___Model_3.launch
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,38 +1,38 @@ | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_3"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="AllSolutions"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;121;0;0"/> | ||
| <listEntry value="P;;5;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> | ||
| <?xml version="1.0" encoding="UTF-8" standalone="no"?> | ||
| <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck"> | ||
| <intAttribute key="autoLockTime" value="15"/> | ||
| <stringAttribute key="configurationName" value="Model_3"/> | ||
| <intAttribute key="dfidDepth" value="100"/> | ||
| <booleanAttribute key="dfidMode" value="false"/> | ||
| <booleanAttribute key="distributedTLC" value="false"/> | ||
| <stringAttribute key="distributedTLCScript" value=""/> | ||
| <stringAttribute key="distributedTLCVMArgs" value=""/> | ||
| <intAttribute key="fpBits" value="0"/> | ||
| <intAttribute key="maxHeapSize" value="500"/> | ||
| <booleanAttribute key="mcMode" value="true"/> | ||
| <stringAttribute key="modelBehaviorInit" value=""/> | ||
| <stringAttribute key="modelBehaviorNext" value=""/> | ||
| <stringAttribute key="modelBehaviorSpec" value=""/> | ||
| <intAttribute key="modelBehaviorSpecType" value="0"/> | ||
| <stringAttribute key="modelBehaviorVars" value=""/> | ||
| <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/> | ||
| <listAttribute key="modelCorrectnessInvariants"/> | ||
| <listAttribute key="modelCorrectnessProperties"/> | ||
| <stringAttribute key="modelExpressionEval" value="AllSolutions"/> | ||
| <stringAttribute key="modelParameterActionConstraint" value=""/> | ||
| <listAttribute key="modelParameterConstants"> | ||
| <listEntry value="N;;121;0;0"/> | ||
| <listEntry value="P;;5;0;0"/> | ||
| </listAttribute> | ||
| <stringAttribute key="modelParameterContraint" value=""/> | ||
| <listAttribute key="modelParameterDefinitions"/> | ||
| <stringAttribute key="modelParameterModelValues" value="{}"/> | ||
| <stringAttribute key="modelParameterNewDefinitions" value=""/> | ||
| <intAttribute key="numberOfWorkers" value="1"/> | ||
| <booleanAttribute key="recover" value="false"/> | ||
| <intAttribute key="simuAril" value="-1"/> | ||
| <intAttribute key="simuDepth" value="100"/> | ||
| <intAttribute key="simuSeed" value="-1"/> | ||
| <stringAttribute key="specName" value="CarTalkPuzzle"/> | ||
| <stringAttribute key="view" value=""/> | ||
| </launchConfiguration> |
Oops, something went wrong.