[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Architecture of the toolbox data



On 11.11.2015 13:04, fl wrote:
> Hi Markus,
>  
> 
>     If you add comments to a launch file outside the Toolbox or change
>     its order, they will be lost during the next Toolbox save. 
> 
> 
> 
> But you can add a widget to your gui can't you? A widget to enter
> a piece of comment.
>  
> 
>     It is incorrect, that the launch files replace the cfg files. 
> 
> 
> They replace the *.cfg files in the sense that it is in the *.launch
> files that the
> use cases are now kept. But I understand they have other information as
> well.
>  
> 
>     A launch file is
>     a superset of a .cfg file content-wise. It e.g. also contains settings
>     about the mode in which TLC gets executed. 
> 
> 
> I have understood that but most of the information is mainly default values
> if you remove them from the *.launch files, you make them more readable
> for the user. I want to emphasize that we need to understand what is
> related to
> the use case outside from your gui. Your gui is very beautiful but
> text-oriented
> information when you are a scientist, an engineer, a technician and so on 
> is important. 
> If you want an analogy, all the sources, makefiles, README, tests
> related to a 
> software can be read with a simple editor as you know. It should be the same
> with what is related to use cases in your implementation.
> 
>  
> 
>     They act as input to generate
>     a cfg file to the *.toolbox/Model_Name/ directory with which TLC
>     eventually gets launched.
> 
> 
> I have understood that. But that way *.cfg files have become temporary
> and unessential files and their true sources are now the launch files
> and the launch files should be
> stored at the same level as the *.tla file just as was the case with the
> *.cfg files. 
> As a rule I think you should separate drastically the essential files 
> from the temporary and ancillary files. (Because that way we only git
> the meaninful files --and use cases are meaningful files-- and throw away 
> the files that are for the machine but not for the human being.) For
> instance
> put all the files we can throw away in *.toolbox directories and *.tla
> and *.launch
> files in the root.
> 
>  
> 
>     What is your real use case that you read and write launch files outside
>     the Toolbox? Applying regular expressions sounds as if you want to
>     mass-edit launch files.
> 
> 
> 
> Yes that's the point. You may want to make a slightly different *.tla
> file and a new
> project without having to enter all the use cases once again but only
> modifying
> them a bit. You may also want to change the name of a constant in all use
> cases without entering again the data that can be sometimes complex 
> (lists, structures etc.)
> 
> Then what I propose is:
> 
> 1) Add a widget to give us the possibility to add a comment.
> 2) Put the launch files at the same level as the *.tla files.
> 3) Don't put default values in the launch files.
> 4) Make clear all what can be regenerated by separated them out
> so that we don't need to git ancillary files (after all we never preserve
> object or log files in a project.) What I propose is *.tla and *.launch in
> the root directory and the rest in *.toolbox directories.

Hi Frederic,

adding a note to a model (free form text) might in fact be a nice
addition to the model editor. Obviously though, this won't be at the
level of individual model parameters.

To create a new model from an existing one, one can use the clone
functionality. It copies everything from the current model to a new one
without the need to re-enter parameters again. What you describe sounds
like clone functionality at the spec level.

Changing constants/actions/... in the spec should just update the
corresponding models. This is a basic refactoring that should be handled
by the Toolbox. A user shouldn't be forced to switch to the command line
and manually change files or run regexps.

Defaults change over time. Adding defaults to the launch files makes
sure that one uses the same value at model creation time rather than any
new value. Using a new default should be a conscious decision.

Moving launch files to the parent folder is a) a major technical change
and b) misses the .project and .settings/ data anyway. I'd rather
suggest to move generated files to a (new) subdirectory instead. Then
the spec files would be at the root and the models in *.toolbox/. All
non-dot toolbox subdirectories could be ignored.

If you want to version your spec and model with e.g. git today, add the
attached .gitignore file to the spec directory. It will include the spec
and the essential model files in the .toolbox directory, but exclude all
files that are generated.

By the way, at some point I hacked on an egit [1] integration for the
Toolbox. With it, specs and models could conveniently be versioned
directly in the spec explorer. I can make the hack available if the
community is willing to continue this effort.

Cheers
Markus

[1] http://www.eclipse.org/egit/

## By default, ignore everything
*
## Do not ignore .gitignore
!/.gitignore
## Do not ignore the spec files
!/*.tla
## Do not ignore the relevant model files/folders
/*.toolbox/*
!/*.toolbox/
!/*.toolbox/.project
!/*.toolbox/*.launch
## Ignore everything in .settings/ except the pref file
/*.toolbox/.settings/*
!/*.toolbox/.settings/
!/*.toolbox/.settings/org.lamport.tla.toolbox.prefs