JacquesCarette / Drasil

Generate all the things (focusing on research software)
https://jacquescarette.github.io/Drasil
BSD 2-Clause "Simplified" License
143 stars 26 forks source link

Relevant Drasil Code for the GlassBR Example #2856

Closed smiths closed 3 years ago

smiths commented 3 years ago

As a follow up to #2855 @balacij, can you propose a subset of the Drasil code that highlights how we go from the Drasil inputs to the outputs for the GlassBR example. In the "Well Understood" paper we will need to show how Drasil facilitates generating all artifacts for software in a well understood domain. The paper is limited to 4 pages, so we won't have much room for this. Don't stress about that too much to start with though. We'll figure out the most important parts of the code as we iterate on the paper.

Don't go too far with this issue before asking for feedback from @JacquesCarette and me.

balacij commented 3 years ago

Thank you Dr. Smith. Would we want specific lines of code to pair with each numbered step in section 3 of the paper?

I think this would show an example of how one can transcribe information for a well-understood domain of knowledge, and how to configure the generators and printers to make use of the information via the existing generators and printers of the well-understood domain.

smiths commented 3 years ago

@balacij, what you describe sounds great, but it is unlikely that we could fit it within the 4 pages of the paper. Maybe this would still be a good systematic way to get started though? If it isn't too time consuming, maybe you could start summarizing the code in this way and then the three of us could discuss?

balacij commented 3 years ago

That sounds good to me, thank you.

I apologize for the length of this post :sweat_smile: . It doesn't actually contain too much information, it's just large because it contains the individual points and spaced out examples. I hope this is an okay starting point.

  1. Have a problem to solve, or task to achieve, which falls in to the realm where software is likely to be the central part of the solution.

    For example, undergraduate-level physics problems.

  2. Convince oneself that the underlying problem domain is well understood, as defined in section 2.

    Section 2's discussion makes this quite clear. I don't think we would need an example regarding this part.

  3. Describe the problem: a. Find the base knowledge (theory) in the pre-existing library or, failing that, write it if it does not yet exist,

    Decomposing the problem spaces required knowledge into all relevant concepts, definitions (DDs too), entity-specific variables and constant data.

    I believe there would be many examples for this. We could pick one of many from any of Assumptions.hs, Concepts.hs, DataDefs.hs, Unitals.hs, and Units.hs.

    For example,

    fullyT, glassTypeFac, heatS, iGlass, lGlass :: CI
    fullyT        = commonIdeaWithDict "fullyT"        (nounPhraseSP "fully tempered")          "FT"       [idglass]
    glassTypeFac  = commonIdeaWithDict "glassTypeFac"  (nounPhraseSP "glass type factor")       "GTF"      [idglass]
    heatS         = commonIdeaWithDict "heatS"         (nounPhraseSP "heat strengthened")       "HS"       [idglass]
    iGlass        = commonIdeaWithDict "iGlass"        (nounPhraseSP "insulating glass")        "IG"       [idglass]
    lGlass        = commonIdeaWithDict "lGlass"        (nounPhraseSP "laminated glass")         "LG"       [idglass]

    Alternatively, a data definition for "risk of failure":

    risk :: DataDefinition
    risk = ddE riskQD
      [dRef astm2009, dRefInfo beasonEtAl1998 $ Equation [4, 5],
      dRefInfo campidelli $ Equation [14]]
      Nothing "riskFun" [aGrtrThanB, hRef, ldfRef, jRef]
      where riskQD = mkQuantDef riskFun riskEq
            riskEq = (sy sflawParamK $/
              (mulRe (sy plateLen) (sy plateWidth) $^ (sy sflawParamM $- exactDbl 1))) `mulRe`
              ((sy modElas `mulRe` square (sy minThick)) $^ sy sflawParamM) `mulRe` sy lDurFac `mulRe` exp (sy stressDistFac)

    b. Assemble the ingredients into a coherent narrative,

    Using figures and natural English, we describe the problem and it's assumptions, and create relations between concepts using the base knowledge as much as possible.

    It's a bit difficult to pick just one example for this because there are so many.

    For example, a system context figure:

    physSystFig :: LabelledContent 
    physSystFig = llcc (makeFigRef "physSystImage") $ figWithWidth 
      (atStartNP $ the physicalSystem) (resourcePath ++ "physicalsystimage.png") 30 

    And a natural description:

    PS1: The glass slab.
    
    PS2: The point of explosion. Where the bomb, or any kind of man-made explosion, is located. The stand off distance is the distance between the point of explosion and the glass.

    via:

    physSystParts :: [Sentence]
    physSystParts = [(atStartNP (the glaSlab)!.),
      foldlSent [(atStartNP (the ptOfExplsn) !.), S "Where the", phrase bomb `sC`
      S "or", (blast ^. defn) `sC` (S "is located" !.), atStartNP (the sD) `S.isThe`
      phrase distance, S "between the", phrase ptOfExplsn `S.and_` phraseNP (the glass)]]

    c. Describe the characteristics of a good solution,

    We can do this in approximately 3 ways: i. Describing what a "solution" means with natural English, and what it would imply. ii. Describing both physical and software output data constraints. iii. Describing the functional and non-functional requirements of the software (e.g., correct, verifiable, understandable, reusable, maintainable, portable).

    For example, the output data constraints:

    stressDistFac, probFail :: ConstrainedChunk
    stressDistFac = cvc "stressDistFac" (nounPhraseSP "stress distribution factor (Function)") 
      cJ Real [physc $ Bounded (Inc, sy stressDistFacMin) (Inc, sy stressDistFacMax)] (Just $ exactDbl 15)
    
    probFail = cvc "probFail" (nounPhraseSP "probability of failure")
      (sub cP lFail) Rational
      [probConstr] (Just $ dbl 0.4)

    And an example of a functional requirement:

    Check-Glass-Safety: If is-safePb ∧ is-safeLR (from TM:isSafeProb and TM:isSafeLoad), output the message "For the given input parameters, the glass is considered safe." If the condition is false, then output the message "For the given input parameters, the glass is NOT considered safe."

    produced by:

    checkGlassSafety :: ConceptInstance 
    checkGlassSafety  = cic "checkGlassSafety" checkGlassSafetyDesc "Check-Glass-Safety" funcReqDom
      where checkGlassSafetyDesc = foldlSent_ [S "If", eS $ sy isSafePb $&& sy isSafeLR,
              sParen (S "from" +:+ refS pbIsSafe `S.and_` refS lrIsSafe) `sC`
              phrase output_, phraseNP (the message), Quote (safeMessage ^. defn),
              S "If the", phrase condition, S "is false, then", phrase output_,
              phraseNP (the message), Quote (notSafe ^. defn)]

    d. Come up with basic examples (to test correctness, intuitions, etc).

    This partially ties in with (3.c). The basic examples (and their solutions) should obey the rules dictated in (3.c). Would we want an example for this?

    e. Identify the naturally occurring known quantities associated to the problem domain, as well as some desired quantities. For example, some problems naturally involve lengths lying in particular ranges, while others will involve ingredient concentrations, again in particular ranges.

    This partially ties in with (3.a).

    For example, a relevant output data (isSafePb), and a component of it's calculation:

    isSafePB, isSafeLR :: QuantityDict
    isSafePb   = vc "isSafePb"   (nounPhraseSP "probability of glass breakage safety requirement")
      (variable "is-safePb")   Boolean
    isSafeLR   = vc "isSafeLR"   (nounPhraseSP "3 second load equivalent resistance safety requirement")
      (variable "is-safeLR")   Boolean
  4. Describe, by successive transformations, how the natural knowledge can be turned from a set of relations (and constraints) into a deterministic input-output process. a. This set of relations might require specializing the theory (eg. from 𝑛-dimensional to 2-dimensional, assuming no friction, etc). These choices need to be documented, and are a crucial aspect of the solution process. The rationale for the choices should also be documented. Lastly, whether these choices are likely or unlikely to change in the future should be recorded.

    We describe how we can take generally applicable theories and refine them for our specific system until they are fully grounded, using relevant named variables (as opposed to generic ones used in theory descriptions). This simplifies the problem into a directed computation (pending formalization in (4.b)).

    For example, we can show how "safety probability" has a grounded version, and it's theoretical version:

    pbIsSafe :: InstanceModel -- Grounded
    pbIsSafe = imNoDeriv (equationalModelN (nounPhraseSP "Safety Req-Pb") pbIsSafeQD)
      [qwC probBr $ UpFrom (Exc, exactDbl 0), qwC pbTol $ UpFrom (Exc, exactDbl 0)]
      (qw isSafePb) []
      [dRef astm2009] "isSafePb"
      [pbIsSafeDesc, probBRRef, pbTolUsr]
        where pbIsSafeQD = mkQuantDef isSafePb (sy probBr $< sy pbTol)
    
    pbIsSafeTM :: TheoryModel
    pbIsSafeTM = tm (equationalModel' pbIsSafeQD) 
      [qw isSafeProb, qw probFail, qw pbTolfail] ([] :: [ConceptChunk])
      [pbIsSafeQD] [] [] [dRef astm2009]
      "isSafeProb" [pbIsSafeDesc]
      where
        pbIsSafeQD = mkQuantDef' isSafeProb (nounPhraseSP "Safety Probability") pbIsSafeExpr
        pbIsSafeExpr = sy probFail $< sy pbTolfail

    b. This set of choices is likely dependent, and thus somewhat ordered. In other words, some decisions will enable other choices to be made that would otherwise be unavailable. Eg: some data involved in the solution process is orderable, so that sorting is now a possibility that may be useful.

    We create a closed harmonic system containing all related knowledge (in particular, the grounded theories), which is as simple as collecting them into a single system.

    iMods :: [InstanceModel]
    iMods = [pbIsSafe, lrIsSafe]
    si :: SystemInformation
    si = SI {
        _sys         = glassBR,
        _kind        = Doc.srs,
        _authors     = [nikitha, spencerSmith],
        _purpose     = purpDoc glassBR Verbose,
        _quants      = symbolsForTable,
        _concepts    = [] :: [DefinedQuantityDict],
        _instModels  = iMods,
        _datadefs    = GB.dataDefs,
        _configFiles = configFp,
        _inputs      = inputs,
        _outputs     = outputs,
        _defSequence = qDefns,
        _constraints = constrained,
        _constants   = constants,
        _sysinfodb   = symbMap,
        _usedinfodb  = usedDB,
         refdb       = refDB
    }
  5. Describe how the computation process from step 4 can be turned into code. Note that the same kinds of choice can occur here.

    We make choices about the software representations of the theories. This would be the focal contents of our Choices.hs file:

    code :: CodeSpec
    code = codeSpec fullSI choices allMods
    
    choices :: Choices
    choices = defaultChoices {
        lang = [Python, Cpp, CSharp, Java, Swift],
        modularity = Modular Separated,
        impType = Program,
        logFile = "log.txt",
        logging = [LogVar, LogFunc],
        comments = [CommentFunc, CommentClass, CommentMod],
        doxVerbosity = Quiet,
        dates = Hide,
        onSfwrConstraint = Exception,
        onPhysConstraint = Exception,
        inputStructure = Bundled,
        constStructure = Inline,
        constRepr = Const,
        auxFiles = [SampleInput "../../datafiles/glassbr/sampleInput.txt", ReadME] 
    }
  6. Turn the steps (i.e. from items 4 and 5) into a recipe, aka program, that weaves together all the information into a variety of artifacts (softifacts). These can be read, or execute, or . . . as appropriate.

    A final executable program which should take the knowledge discussed above, and use premade printers/generators to generate software artifacts, SRS documents, etc.

    main :: IO()
    main = do
        setLocaleEncoding utf8
        gen (DocSpec (docChoices SRS [HTML, TeX]) "GlassBR_SRS") srs printSetting
        genCode choices code
        genDot fullSI
        genLog fullSI printSetting
smiths commented 3 years ago

Great work @balacij. I actually misunderstood what you were going to do, and I like what you did better than what I thought you were going to do. :smile: I thought you were looking at the code needed to generate the outputs in the GlassBR Inputs to Artifact Outputs figure, but what you have tackled has a nice connection to the "ideal process." The nice thing is that we can reuse the code examples to also explain some of what is generated in the GlassBR figure. In a sense you did do what I thought you were doing, but approaching it from a different perspective.

I'm still worried about the length, but we can postpone that distraction for now.

I have some preliminary thoughts as follows:

balacij commented 3 years ago

Thank you Dr. Smith, I'm happy it was better than what you were expecting!

Sounds good. I hope it won't be too much of an issue.

I wonder if we could pick a single output variable and build up a graph showing all chunks that it references (down to the input variables and their information). Would this be closer to what you were expecting/wanting?

balacij commented 3 years ago

For 3b, I like the idea of using the goal statement @smiths, it makes more sense than the figure code.

Predict-Glass-Withstands-Explosion: Analyze and predict whether the glass slab under consideration will be able to withstand the explosion of a certain degree which is calculated based on user input.

generated via:

willBreakGS :: ConceptInstance
willBreakGS = cic "willBreakGS" (foldlSent [S "Analyze" `S.and_`
  S "predict whether the", phrase glaSlab, S "under consideration will be able",
  S "to withstand the", phrase explosion `S.of_` S "a certain", phrase degree_',
  S "which is calculated based on", phrase userInput])
  "Predict-Glass-Withstands-Explosion" goalStmtDom

Regarding 3.c, would we potentially want to add that as a functional requirement to GlassBR as well?

For 4.a, I was initially thinking about using a derivation, but we don't seem to have any in GlassBR. Is this something that should be added for variable substitution at least?

Some of the assumptions:

glassType: The standard E1300-09a for calculation applies only to monolithic, laminated, or insulating glass constructions of rectangular shape with continuous lateral support along one, two, three, or four edges. This practice assumes that: (1) the supported glass edges for two, three and four-sided support conditions are simply supported and free to slip in plane; (2) glass supported on two sides acts as a simply supported beam; and (3) glass supported on one side acts as a cantilever.

glassCondition: Following astm2009 (pg. 1), this practice does not apply to any form of wired, patterned, etched, sandblasted, drilled, notched, or grooved glass with surface and edge treatments that alter the glass strength. (RefBy: UC:Accommodate-Altered-Glass.)

boundaryConditions: Boundary conditions for the glass slab are assumed to be 4-sided support for calculations. (RefBy: LC:Accomodate-More-Boundary-Conditions.)

written via:

glassTypeDesc :: Sentence
glassTypeDesc = foldlSent [S "The standard E1300-09a for",
  phrase calculation, S "applies only to", foldlList Comma Options $ map S ["monolithic",
  "laminated", "insulating"], S "glass constructions" `S.of_` S "rectangular", phrase shape, 
  S "with continuous", phrase lateral, S "support along",
  foldlList Comma Options (map S ["one", "two", "three", "four"]) +:+.
  plural edge, S "This", phrase practice +: S "assumes that",
  foldlEnumList Numb Parens SemiCol List $ map foldlSent_
  [[S "the supported glass", plural edge, S "for two, three" `S.and_`
  S "four-sided support", plural condition, S "are simply supported" `S.and_`
  S "free to slip in", phrase plane], 
  [S "glass supported on two sides acts as a simply supported", phrase beam], 
  [S "glass supported on one side acts as a", phrase cantilever]]]

glassConditionDesc :: Sentence
glassConditionDesc = foldlSent [S "Following", complexRef astm2009 (Page [1]) `sC` 
  S "this", phrase practice, S "does not apply to any form of", foldlList Comma Options $ map S ["wired",
  "patterned", "etched", "sandblasted", "drilled", "notched", "grooved glass"], S "with", 
  phrase surface `S.and_` S "edge treatments that alter the glass strength"]

boundaryConditionsDesc :: Sentence
boundaryConditionsDesc = foldlSent [S "Boundary", plural condition, S "for the",
  phrase glaSlab, S "are assumed to be 4-sided support for",
  plural calculation]
smiths commented 3 years ago

From above:

I wonder if we could pick a single output variable and build up a graph showing all chunks that it references (down to the input variables and their information). Would this be closer to what you were expecting/wanting?

I'm not sure exactly what you are getting at here, but you might be on to something. Could you give an example? Don't go to the work of drawing a graph yet. To start with you could describe an example in words, and then we can decide how far to pursue the idea.

For 3c we can't add any of the conservation laws to GlassBR because GlassBR is a phenomenological model. It is based on empirical data, not first principles physics. We can add conservation of energy to projectile motion (the sum of kinetic energy and potential energy should be constant over time), but that isn't worth the effort of pursuing right now. We won't have time in 4 pages to give that many examples. We can just use words to describe how we use the properties of a correct solution to verify a solution.

The example that P_b is bounded between 0 and 1 would be a good example for 3c. We know there is a mistake in our calculations if this constraint is violated. As an aside, do you know why IM:isSafePb in GlassBr shows the lower bound for P_b (0), but not the upper bound (1)? I would have thought that the input constraint in IM:isSafePb would come from the same place as information in the Data Constraints Table in section "Properties of a Correct Solution". We don't need to worry about this right now for the paper, but it is something to look at later.

For 4a, I looked at places where we could add a derivation to GlassBR, but since it is a phenomenological example (as mentioned above) I didn't find any candidate spots. The assumptions listed for GlassBR aren't really used in the derivation of any of the chunks. They are more used to fill in values in the chunks.

balacij commented 3 years ago

I'm not sure exactly what you are getting at here, but you might be on to something. Could you give an example? Don't go to the work of drawing a graph yet. To start with you could describe an example in words, and then we can decide how far to pursue the idea.

Yes, for example, with IM:isSafePb, it references Pb and Pbtol, then Pb references B, and then B references k, a, b, m, E, h, LDF, and J. Each of those variables would be a node below IM:isSafePb. We might also have a node above IM:isSafePb for TM:isSafeProb, showing that it's an instance of TM:isSafeProb. With each arrow, we could write a generic classifier for the relationship between the nodes. The graph might be fairly simple, but it could potentially be a good candidate for showing how Drasil wants all possible information about an output, and traces its relationships to the inputs (and other information).

For 3c we can't add any of the conservation laws to GlassBR because GlassBR is a phenomenological model. It is based on empirical data, not first principles physics. We can add conservation of energy to projectile motion (the sum of kinetic energy and potential energy should be constant over time), but that isn't worth the effort of pursuing right now. We won't have time in 4 pages to give that many examples. We can just use words to describe how we use the properties of a correct solution to verify a solution.

That's interesting. I wasn't aware of that! Out of curiosity, should that explanation for the origin of the equation be discussed where the derivation would normally be? Though, it would probably be also discussed in the source references.

The example that P_b is bounded between 0 and 1 would be a good example for 3c. We know there is a mistake in our calculations if this constraint is violated. As an aside, do you know why IM:isSafePb in GlassBr shows the lower bound for P_b (0), but not the upper bound (1)? I would have thought that the input constraint in IM:isSafePb would come from the same place as information in the Data Constraints Table in section "Properties of a Correct Solution". We don't need to worry about this right now for the paper, but it is something to look at later.

Looking at the code for this InstanceModel, it appears to be manually filled in, not shared with the constraints from the input data constraints table. It looks like this will need to be fixed then.

For 4a, I looked at places where we could add a derivation to GlassBR, but since it is a phenomenological example (as mentioned above) I didn't find any candidate spots. The assumptions listed for GlassBR aren't really used in the derivation of any of the chunks. They are more used to fill in values in the chunks.

Yes. If I'm understanding it correctly, this might be a bit difficult to directly show right now. It might be something that is better highlighted when we've built the system that Dr. Carette briefly mentioned in https://github.com/JacquesCarette/Drasil/issues/2599#issuecomment-863593619 where we might have NewThy = ApplyRefinement R1 (ApplyRefinment R2 Thy))-like code to refine models.

smiths commented 3 years ago

Yes, for example, with IM:isSafePb, it references Pb and Pbtol, then Pb references B, and then B references k, a, b, m, E, h, LDF, and J. Each of those variables would be a node below IM:isSafePb. We might also have a node above IM:isSafePb for TM:isSafeProb, showing that it's an instance of TM:isSafeProb. With each arrow, we could write a generic classifier for the relationship between the nodes. The graph might be fairly simple, but it could potentially be a good candidate for showing how Drasil wants all possible information about an output, and traces its relationships to the inputs (and other information).

Yes, I get what you are saying. I think this is a great idea. This kind of traceability information is great to see. It will help people understand Drasil, and it will show how we can help manage change. Please proceed with drawing the figure when you have time. If we don't use it for the paper (because of space limitations), you can use it in your thesis document and we can use it in future papers.

For 3c we can't add any of the conservation laws to GlassBR because GlassBR is a phenomenological model. It is based on empirical data, not first principles physics. We can add conservation of energy to projectile motion (the sum of kinetic energy and potential energy should be constant over time), but that isn't worth the effort of pursuing right now. We won't have time in 4 pages to give that many examples. We can just use words to describe how we use the properties of a correct solution to verify a solution.

That's interesting. I wasn't aware of that! Out of curiosity, should that explanation for the origin of the equation be discussed where the derivation would normally be? Though, it would probably be also discussed in the source references.

At the moment we are leaving it to the source reference to present the origin of the equation. We could definitely use the derivation section to expand on what is currently provided. The derivations were added to the template when extra information was needed to explain the connection between chunks. We can add a "derivation" whenever we have more information to share. I don't think we need to add more information in GlassBr, but if it would help the paper, we could do an example like this.

For 4a, I looked at places where we could add a derivation to GlassBR, but since it is a phenomenological example (as mentioned above) I didn't find any candidate spots. The assumptions listed for GlassBR aren't really used in the derivation of any of the chunks. They are more used to fill in values in the chunks.

Yes. If I'm understanding it correctly, this might be a bit difficult to directly show right now. It might be something that is better highlighted when we've built the system that Dr. Carette briefly mentioned in #2599 (comment) where we might have NewThy = ApplyRefinement R1 (ApplyRefinment R2 Thy))-like code to refine models.

Yes, I agree.

smiths commented 3 years ago

@balacij, do you think you could make an attempt to put the Drasil code into the paper now? We've freed up about 1 page with our latest edits. There is a spot marked in the paper (marked TODO : Jason - insert the code examples for the ideal process here) where the examples should go.

You don't have to worry too much about editing, just focus on getting the material into the paper. I'd like to know how much space it takes up, and then we can focus on prioritizing what should stay.

balacij commented 3 years ago

I just posted the latest examples discussed on the document. However, I used the verbatim block for the code, which doesn't appear to work very well with the 2 column format (it doesn't seem to be doing any sort of word wrapping).

We still had a few points left without an "example" because they either require a discussion, or require clarification to produce a code example.

smiths commented 3 years ago

Thank you @balacij. I don't think verbatim will work. I'm doing a pass right now to switch the code to the listings package. We won't be able to incorporate everything, given the space limitations. We'll discuss with @JacquesCarette, once he has read the paper.

smiths commented 3 years ago

I've changed to the listings environment in 93e402445. I took out the enum environment as well, since we won't have room for all of it, and the structure will be lost to the reader given the size of the example, and the 2 column format. I've replaced it with subsections. I think we should pick a few pieces of the process to emphasize, rather than the entire process. We just don't have room. We can discuss with @JacquesCarette what pieces of the process to emphasize. For some of the code snippets, I'm not really sure where they belong in the process. We can discuss that as well. :smile:

balacij commented 3 years ago

That change is very neat! The formatting is a lot better. I didn't know about that \lstset had all of those options, this (+ the formatting change) is certainly good for future reference for me. Thank you!

We just don't have room. We can discuss with @JacquesCarette what pieces of the process to emphasize. For some of the code snippets, I'm not really sure where they belong in the process. We can discuss that as well. :smile:

Sounds good. I will try to complete the other picture example today. I'm trying to use LaTeX, but it seems to be giving me problems with the size of nodes. I might just use Draw.io for it as well.

smiths commented 3 years ago

Yes, the listings package is very helpful. It will definitely come in handy when you are writing your thesis! :smile:

For the other picture, don't stress about making it look perfect. We might not even have room in the paper. If you can make it so the figure would fit within a column width, instead of needing to be two columns, that would help.

JacquesCarette commented 3 years ago

I've just pushed a big edit of title-abstract-section 1 (and merged with the listings change).

smiths commented 3 years ago

I've had a quick look over the changes and I like them. Nice and punchy. :smile: I noticed at least one minor grammar issue, so I'll do an editorial pass through the section now.

smiths commented 3 years ago

In b1f72df87 I pushed a new version of the abstract. The only real change is that I replaced "this" with "productivity". It just wasn't clear what the "this" was referring to.

There was a merge conflict. I think I kept the incoming changes, so everything should be fine, but it is showing the text about choices as uncommented. @JacquesCarette, if you planned to comment this out, I may have inadvertently undone this change.

JacquesCarette commented 3 years ago

Yes, I meant to comment that out (for now). Merging now.

balacij commented 3 years ago

Yes, I get what you are saying. I think this is a great idea. This kind of traceability information is great to see. It will help people understand Drasil, and it will show how we can help manage change. Please proceed with drawing the figure when you have time. If we don't use it for the paper (because of space limitations), you can use it in your thesis document and we can use it in future papers.

In 96cba8d537493ccc1e91856580d5852aec94c20c, I started working on a TikZ picture for this. I'm not sure if it would be suitable for the paper, however, but it's starting to look kind of nice!

EDIT: I wonder if this is something that we can reasonably generate ourselves soon too.

smiths commented 3 years ago

I like how your picture is shaping up @balacij. I have been working on something similar (very sporadically) to try and visualizes the refinement of theories. Pictures like this are very helpful to organize our thoughts. The idea of generating these pictures is exciting. My guess is that we'll need to really nail down what we mean by refinement before it will be possible, but then a picture as a different view of the information that is in the code should be feasible.

I have a minor request for the figure. Instead of $is-safeProb$ can you use $\mathit{is\_safeProb}$. I know it is the first way in the generated LaTeX SRS, but I've never liked it. :smile: It looks like the dash is a minus sign. Also, LaTeX spaces all the characters as if they are variables that are multiplied together. Although it is a low priority, I would like us to fix the symbol in the LaTeX document as well.

balacij commented 3 years ago

The idea of generating these pictures is exciting. My guess is that we'll need to really nail down what we mean by refinement before it will be possible, but then a picture as a different view of the information that is in the code should be feasible.

It certainly is! Yes, I agree. The connections will certainly be difficult without the refinement information.

I have a minor request for the figure. Instead of $is-safeProb$ can you use $\mathit{is_safeProb}$. I know it is the first way in the generated LaTeX SRS, but I've never liked it.

Thank you! I was trying to use \texttt to make it look more "normal", but it was a bit awkward. This is a definite improvement. This change is reflected in 00e590270312d04d7a98795993bb3e38143d05a1.

It looks like the dash is a minus sign. Also, LaTeX spaces all the characters as if they are variables that are multiplied together. Although it is a low priority, I would like us to fix the symbol in the LaTeX document as well.

Yes, I agree. Out of curiosity, would the solution be as simple as checking if a string contains multiple concatenated characters in it's symbol? If so, I'm sure this is something that could be fixed easily. It would also be nice to fix the other issue you mentioned (on another ticket) where multiplication of multiple multi-character symbols ends up looking like one long multi-character symbol.

smiths commented 3 years ago

The figure looks much nicer. Thank you @balacij.

If we could fix the formatting of multi-character variables names in LaTeX that would be great. It would be great if it is as simple as checking for multi-character strings. My first thought is that it is probably more complex than that, since it hasn't already been fixed, but we haven't prioritized the formatting, so maybe nobody really looked at a solution?

I looked through the issue tracker and I found one issue that mentions this problem: #1853. The only discussion is the implied conversation about whether to fix long variable names by making them in italics, or to use a sans serif solution. I remember now that this issue was discussed at the time, but there wasn't any convergence on what behaviour we wanted. I don't think we discussed how to actually make the fix.

If it is easy to do, maybe we could go ahead with the $\mathit{multicharactervariablename}$ fix for now, and make this user configurable in the future? The variable names are currently distracting in the LaTeX version of the documents.