diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index d7b935872c..e13a8fa14f 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -820,7 +820,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function && !PrimitiveType.Null.IsSameTypeAs(assignStmt.Value.Type) && !PrimitiveType.Any.IsSameTypeAs(assignStmt.Location.Type); WriteLValue(context, output, assignStmt.Location); - context.Write(output, $" = ({GetCSharpType(assignStmt.Location.Type)})("); + context.Write(output, $" = ({GetCSharpType(assignStmt.Location.Type, true)})("); if (needCtorAdapter) { context.Write(output, $"new {GetCSharpType(assignStmt.Location.Type)}("); diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NullLiteralExpr.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NullLiteralExpr.cs index 06cb81f3df..f44a8ed0b3 100644 --- a/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NullLiteralExpr.cs +++ b/Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NullLiteralExpr.cs @@ -12,6 +12,6 @@ public NullLiteralExpr(ParserRuleContext sourceLocation) public ParserRuleContext SourceLocation { get; } - public PLanguageType Type { get; } = PrimitiveType.Any; + public PLanguageType Type { get; } = PrimitiveType.Null; } } \ No newline at end of file diff --git a/Tst/RegressionTests/Feature4DataTypes/StaticError/nullComparison/nullType.p b/Tst/RegressionTests/Feature4DataTypes/StaticError/nullComparison/nullType.p new file mode 100644 index 0000000000..f8b9afc1d3 --- /dev/null +++ b/Tst/RegressionTests/Feature4DataTypes/StaticError/nullComparison/nullType.p @@ -0,0 +1,10 @@ +machine Main { + start state Init { + entry { + var x: int; + if(x == null) { + + } + } + } + } \ No newline at end of file diff --git a/Tst/RegressionTests/Feature4DataTypes/StaticError/nullTypeAssign/nullType.p b/Tst/RegressionTests/Feature4DataTypes/StaticError/nullTypeAssign/nullType.p new file mode 100644 index 0000000000..2244d3e3c2 --- /dev/null +++ b/Tst/RegressionTests/Feature4DataTypes/StaticError/nullTypeAssign/nullType.p @@ -0,0 +1,8 @@ +machine Main { + start state Init { + entry { + var x: int; + x = null to int; + } + } + } \ No newline at end of file diff --git a/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs b/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs deleted file mode 100644 index 8c9ce3176f..0000000000 --- a/Tutorial/2_TwoPhaseCommit/PForeign/ForeignCode.cs +++ /dev/null @@ -1,22 +0,0 @@ -using System; -using System.Runtime; -using System.Collections.Generic; -using System.Linq; -using System.IO; -using PChecker.PRuntime; -using PChecker.PRuntime.Values; -using PChecker.PRuntime.Exceptions; -using System.Threading; -using System.Threading.Tasks; - -#pragma warning disable 162, 219, 414 -namespace PImplementation -{ - public static partial class GlobalFunctions - { - public static PrtNamedTuple ChooseRandomTransaction(PrtInt uniqueId, PMachine pMachine) - { - return (new PrtNamedTuple(new string[] { "key", "val", "transId" }, (PrtString)pMachine.TryRandomInt(10).ToString(), (PrtInt)pMachine.TryRandomInt(10), (PrtInt) uniqueId)); - } - } -} \ No newline at end of file diff --git a/Tutorial/2_TwoPhaseCommit/PForeign/GlobalFunctions.java b/Tutorial/2_TwoPhaseCommit/PForeign/GlobalFunctions.java deleted file mode 100644 index a9165085a4..0000000000 --- a/Tutorial/2_TwoPhaseCommit/PForeign/GlobalFunctions.java +++ /dev/null @@ -1,25 +0,0 @@ -package psym.model; - -import psym.runtime.values.*; -import java.util.ArrayList; -import java.util.List; -import java.util.HashMap; -import java.util.Map; -import java.util.Random; - -public class GlobalFunctions { - public static PNamedTuple ChooseRandomTransaction(PInt uniqueId) { - List fields = new ArrayList<>(); - fields.add("key"); - fields.add("val"); - fields.add("transId"); - - Map> values = new HashMap<>(); - Random rand = new Random(); - values.put("key", new PString(String.format("%d", rand.nextInt(10)))); - values.put("val", new PInt(rand.nextInt(10))); - values.put("transId", new PInt(uniqueId)); - - return new PNamedTuple(fields, values); - } -} diff --git a/Tutorial/2_TwoPhaseCommit/PTst/Client.p b/Tutorial/2_TwoPhaseCommit/PTst/Client.p index c32d39a393..1cb7548dc0 100644 --- a/Tutorial/2_TwoPhaseCommit/PTst/Client.p +++ b/Tutorial/2_TwoPhaseCommit/PTst/Client.p @@ -55,9 +55,10 @@ machine Client { } } -/* This is an external function (implemented in C#) to randomly choose transaction values -In P, function declarations without body are considered as foreign functions. */ -fun ChooseRandomTransaction(uniqueId: int): tTrans; +fun ChooseRandomTransaction(uniqueId: int): tTrans { + return (key = format("{0}", choose(10)), val = choose(10), transId = uniqueId); +} + // two phase commit client module module TwoPCClient = { Client }; diff --git a/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs b/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs index a9d0170b5d..d1c4df1d0e 100644 --- a/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs +++ b/Tutorial/PriorityQueue/PForeign/ClientFunctions.cs @@ -1,5 +1,5 @@ using System.Collections; -using PChecker.PRuntime.Values; +using PChecker.Runtime.Values; namespace PImplementation { @@ -9,7 +9,7 @@ namespace PImplementation */ partial class Client { - public static tPriorityQueue AddIntToQueue(tPriorityQueue queue, IPrtValue elem, PrtInt priority) + public static tPriorityQueue AddIntToQueue(tPriorityQueue queue, IPValue elem, PInt priority) { queue.Add(new ElementWithPriority(elem, priority)); return queue; diff --git a/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs b/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs index 986c7d0f9b..c2a5e67f06 100644 --- a/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs +++ b/Tutorial/PriorityQueue/PForeign/PriorityQueue.cs @@ -4,9 +4,9 @@ using System.Linq; using System.IO; using System.Linq.Expressions; -using PChecker.PRuntime; -using PChecker.PRuntime.Values; -using PChecker.PRuntime.Exceptions; +using PChecker.Runtime; +using PChecker.Runtime.Values; +using PChecker.Runtime.Exceptions; using System.Threading; using System.Threading.Tasks; @@ -21,7 +21,7 @@ Apart from that the implementation of the foreign type can be arbitrary sequenti If you want to pretty print the foreign type value, you can also override the ToString() function in their implementation. */ - public class tPriorityQueue : IPrtValue + public class tPriorityQueue : IPValue { // naive implementation of the priority queue as a list of elements with priority private List elements = new List(); @@ -39,14 +39,14 @@ public void Delete(ElementWithPriority elem) } // priority remove - public IPrtValue PriorityRemove() + public IPValue PriorityRemove() { var removeElem = elements.OrderBy(el => el.Priority).First(); elements.Remove(removeElem); return removeElem.Element; } - public bool Equals(IPrtValue other) + public bool Equals(IPValue other) { if (other is tPriorityQueue || other != null) { @@ -58,7 +58,7 @@ public bool Equals(IPrtValue other) } } - public IPrtValue Clone() + public IPValue Clone() { var cloned = new tPriorityQueue(); foreach (var elem in elements) @@ -73,7 +73,7 @@ public int Size() return elements.Count; } - public IPrtValue GetElementAt(int index) + public IPValue GetElementAt(int index) { return elements.ElementAt(index).Element; } @@ -81,10 +81,10 @@ public IPrtValue GetElementAt(int index) public class ElementWithPriority { - public IPrtValue Element { get; } + public IPValue Element { get; } public int Priority { get; } - public ElementWithPriority(IPrtValue elem, int priority) + public ElementWithPriority(IPValue elem, int priority) { Element = elem; Priority = priority; diff --git a/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs b/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs index 9f69a5ad67..bbbde28346 100644 --- a/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs +++ b/Tutorial/PriorityQueue/PForeign/PriorityQueueFunctions.cs @@ -7,9 +7,10 @@ using System.Collections.Generic; using System.Linq; using System.IO; -using PChecker.PRuntime; -using PChecker.PRuntime.Values; -using PChecker.PRuntime.Exceptions; +using PChecker.Runtime; +using PChecker.Runtime.Values; +using PChecker.Runtime.Exceptions; +using PChecker.Runtime.StateMachines; using System.Threading; using System.Threading.Tasks; @@ -21,27 +22,27 @@ namespace PImplementation // Also, all global foreign functions must be declared static! public static partial class GlobalFunctions { - public static tPriorityQueue CreatePriorityQueue(PMachine machine) + public static tPriorityQueue CreatePriorityQueue(StateMachine machine) { // use these log statements if you want logs in the foreign code to show up in the error trace. machine.LogLine("Creating Priority Queue!"); return new tPriorityQueue(); } - public static tPriorityQueue AddElement(tPriorityQueue queue, IPrtValue elem, PrtInt priority, PMachine machine) + public static tPriorityQueue AddElement(tPriorityQueue queue, IPValue elem, PInt priority, StateMachine machine) { queue.Add(new ElementWithPriority(elem, priority)); machine.LogLine("Adding Element in the Priority Queue!"); return queue; } - public static PrtNamedTuple RemoveElement(tPriorityQueue queue, PMachine machine) + public static PNamedTuple RemoveElement(tPriorityQueue queue, StateMachine machine) { var element = queue.PriorityRemove(); - var retVal = new PrtNamedTuple(new string[] { "element", "queue" }, new IPrtValue[] { element, queue }); + var retVal = new PNamedTuple(new string[] { "element", "queue" }, new IPValue[] { element, queue }); return retVal; } - public static PrtInt CountElement(tPriorityQueue queue, PMachine machine) + public static PInt CountElement(tPriorityQueue queue, StateMachine machine) { return queue.Size(); } @@ -49,11 +50,11 @@ public static PrtInt CountElement(tPriorityQueue queue, PMachine machine) /* * Modeling Nondeterminism or Randomness in Foreign Functions */ - public static IPrtValue ChooseElement(tPriorityQueue queue, PMachine machine) + public static IPValue ChooseElement(tPriorityQueue queue, StateMachine machine) { // one can write a nondeterministic foreign function using the machine.*Random functions. // all machine.TryRandom*() functions are controlled by the P checker during exploration. - var index = machine.TryRandomInt(queue.Size()); + var index = (PInt)machine.TryRandom((PInt)queue.Size()); machine.LogLine("Choosing element at location: " + index); return queue.GetElementAt(index); }