Update AGREE to use JKind v4.0

[kfhoech]

JKind 4.0 is available. When should AGREE update to use this?

Impacts:

1. The interface to jkind.lustre.Program has changed to accommodate uninterpreted functions. Since AGREE does not yet use these, this should be a low-impact change. Classes affected are LustreAstBuilder, AgreeMakeClockedLustreNodes, LustreCondactNodeVisitor, and LustreContractAstBuilder. Also affected is the TCG in GenerateUfcObligationsVisistor.

2. The interface to jkind.lustre.visitors.TypeReconstructor has changed to require the JLustre program be supplied at construction. This makes the TCG class GenerateUfcObligationsVisistor have awkward handling of the program state, This will need to be refactored at a low-to-moderate impact.

3. The interface to jkind.translation.InlineNodeCalls has changed. Rather than producing a top-level node, a program is produced. How does this affect subsequent application of other translation visitors?

4. The interface to ExprVisitor now adds a FunctionCallExpr. This is due to the addition of uninterpreted functions and is a very low-impact change. Classes affected are AgreeCycleVisitor, IdGatherer, IdRewriteVisitor, NumericEvaluator, SynbolicEvaluator, PrettyPrintVisitor and their subclasses. Also affected is the TCG in GenerateUfcObligationsVisistor.

5. Interval generalization has been removed. This affects the display of results in the counter example viewers in AgreeMenuListener. Also affected is the TCG in TcgXmlWriter, TestCaseGeneratorMenuListener, and TestSuiteMenuListener. This is likely to be a low-impact change as long as the interval display is no longer required.

[mwwhalen]

Hi all. My 2c is below.

On Mon, Feb 26, 2018 at 2:25 PM, kfhoech ***@***.***> wrote: JKind 4.0 is available. When should AGREE update to use this?

Why not soon? I will handle the TCG impact if you like. We could create a jkind 4.0 branch and I think relatively quickly manage the TCG-related stuff. I know I was using the Type Reconstructor for another purpose recently - I will have to figure out where this was.

Impacts: 1. The interface to jkind.lustre.Program has changed to accommodate uninterpreted functions. Since AGREE does not yet use these, this should be a low-impact change. Classes affected are LustreAstBuilder, AgreeMakeClockedLustreNodes, LustreCondactNodeVisitor, and LustreContractAstBuilder. Also affected is the TCG in GenerateUfcObligationsVisistor. 2. The interface to jkind.lustre.visitors.TypeReconstructor has changed to require the JLustre program be supplied at construction. This makes the TCG class GenerateUfcObligationsVisistor have awkward handling of the program state, This will need to be refactored at a low-to-moderate impact. As long as we pass in the program to the GenerateUfcObligationsVisitor, I

think that this should be o.k. with minimal impact.

1. 2. The interface to jkind.translation.InlineNodeCalls has changed. Rather than producing a top-level node, a program is produced. How does this affect subsequent application of other translation visitors? 3. The interface to ExprVisitor now adds a FunctionCallExpr. This is due to the addition of uninterpreted functions and is a very low-impact change. Classes affected are AgreeCycleVisitor, IdGatherer, IdRewriteVisitor, NumericEvaluator, SynbolicEvaluator, PrettyPrintVisitor and their subclasses. Also affected is the TCG in GenerateUfcObligationsVisistor. 4. Interval generalization has been removed. This affects the display of results in the counter example viewers in AgreeMenuListener. Also affected is the TCG in TcgXmlWriter, TestCaseGeneratorMenuListener, and TestSuiteMenuListener. This is likely to be a low-impact change as long as the interval display is no longer required.

This sounds like more an issue of removing things than adding them. I am always happy to shrink my codebase :).

…

1. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#83>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AE-auuBFnpYY0n9U9Wp9ZsNXQyC6iffQks5tYxM-gaJpZM4ST3uL> .

-- Michael Whalen Director, University of Minnesota Software Engineering Center (UMSEC) 200 Union St. 4-192 Minneapolis, MN 55455 Office: 612-624-5130 Cell: 651-442-8834

[lgwagner]

Best to get the latest, IMO. He fixed a PDR bug last week that is not in 4.0. It may not bite you, but it did bite me on an internal project. Lucas On Mon, Feb 26, 2018 at 3:02 PM, Michael Whalen <notifications@github.com> wrote:

…

Hi all. My 2c is below. On Mon, Feb 26, 2018 at 2:25 PM, kfhoech ***@***.***> wrote: > JKind 4.0 is available. When should AGREE update to use this? > Why not soon? I will handle the TCG impact if you like. We could create a jkind 4.0 branch and I think relatively quickly manage the TCG-related stuff. I know I was using the Type Reconstructor for another purpose recently - I will have to figure out where this was. > Impacts: > > 1. > > The interface to jkind.lustre.Program has changed to accommodate > uninterpreted functions. Since AGREE does not yet use these, this should be > a low-impact change. Classes affected are LustreAstBuilder, > AgreeMakeClockedLustreNodes, LustreCondactNodeVisitor, and > LustreContractAstBuilder. Also affected is the TCG in > GenerateUfcObligationsVisistor. > 2. > > The interface to jkind.lustre.visitors.TypeReconstructor has changed > to require the JLustre program be supplied at construction. This makes the > TCG class GenerateUfcObligationsVisistor have awkward handling of the > program state, This will need to be refactored at a low-to-moderate impact. > > As long as we pass in the program to the GenerateUfcObligationsVisitor, I think that this should be o.k. with minimal impact. > > 1. > 2. > > The interface to jkind.translation.InlineNodeCalls has changed. Rather > than producing a top-level node, a program is produced. How does this > affect subsequent application of other translation visitors? > 3. > > The interface to ExprVisitor now adds a FunctionCallExpr. This is due > to the addition of uninterpreted functions and is a very low-impact change. > Classes affected are AgreeCycleVisitor, IdGatherer, IdRewriteVisitor, > NumericEvaluator, SynbolicEvaluator, PrettyPrintVisitor and their > subclasses. Also affected is the TCG in GenerateUfcObligationsVisistor. > 4. > > Interval generalization has been removed. This affects the display of > results in the counter example viewers in AgreeMenuListener. Also affected > is the TCG in TcgXmlWriter, TestCaseGeneratorMenuListener, and > TestSuiteMenuListener. This is likely to be a low-impact change as long as > the interval display is no longer required. > > This sounds like more an issue of removing things than adding them. I am always happy to shrink my codebase :). > > 1. > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#83>, or mute the thread > <https://github.com/notifications/unsubscribe-auth/AE- auuBFnpYY0n9U9Wp9ZsNXQyC6iffQks5tYxM-gaJpZM4ST3uL> > . > -- Michael Whalen Director, University of Minnesota Software Engineering Center (UMSEC) 200 Union St <https://maps.google.com/?q=200+Union+St&entry=gmail&source=g>. 4-192 Minneapolis, MN 55455 Office: 612-624-5130 <(612)%20624-5130> Cell: 651-442-8834 <(651)%20442-8834> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#83 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACkvrdqKrFa6vh4GasnBFO1SH0fqocAUks5tYxvmgaJpZM4ST3uL> .

[kfhoech]

Agreed that we should get the PDR fix. But for sanity in being able to replicate builds, we should have JKind at a release, or at least at some tag we can reproduce.

And, yes most of these changes are removing items from the code base and are low impact. The only one that I'm uncertain about is the change to AgreeNodeToLustreContract due to the change to InlineNodeCalls. The output of the latter changed from a Node to a Program. Given that other visitors in the former depend on its output being a Node, is the right thing to do to iterate over the nodes in the resulting program? It seems that's the right thing to do.

[kfhoech]

And, there's a couple of changes to the Simulator too... But it looks as if these are only to do with adding the case to visitors for the FunctionCallExpr.

[mwwhalen]

Karl, I would guess that the resultant program is a single node program with zero or more function specifications. If we are not using uninterpreted functions in AGREE, and my supposition is correct, we can immediately extract the node. Mike

…

On Mon, Feb 26, 2018 at 3:25 PM, kfhoech ***@***.***> wrote: And, there's a couple of changes to the Simulator too... But it looks as if these are only to do with adding the case to visitors for the FunctionCallExpr. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#83 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AE-aulPLshoGZmecptrST0nLLbZ8Lqx3ks5tYyE6gaJpZM4ST3uL> .

-- Michael Whalen Director, University of Minnesota Software Engineering Center (UMSEC) 200 Union St. 4-192 Minneapolis, MN 55455 Office: 612-624-5130 Cell: 651-442-8834

[kfhoech]

A new branch develop_jkind4 has been created for the upgrade to JKind v4.

[kfhoech]

Resolved by Pull Request 87.