Skip to content

Instantly share code, notes, and snippets.

@jarjuk

jarjuk/model.cfg

Created April 25, 2016 08:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jarjuk/ff81790411095fca5b08fb7a9111b2d7 to your computer and use it in GitHub Desktop.
Save jarjuk/ff81790411095fca5b08fb7a9111b2d7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
model.cfg
SPECIFICATION Spec
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.
Raw
model.old
Model version: 0.0.1-SNAPSHOT
Generator version: 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
------------------------------ MODULE model ------------------------------
EXTENDS TLC, FiniteSets, Sequences, Naturals
(* Execution environment *)
CONSTANTS Steps \* Sequence process/parameter records
(* Magic values *)
CONSTANTS WildCard \* bind to any value
CONSTANTS Nil \* no value
(******************************************************************
Extension point for constants
- modelData none
- template extend/extend_const.mustache
******************************************************************)
(******************************************************************
Domain definitions
- modelData domains
- template domains.mustache
******************************************************************)
CONSTANTS d_name
CONSTANTS d_street
CONSTANTS d_city
CONSTANTS d_lead_id
CONSTANTS d_not_used
CONSTANTS d_account_id
CONSTANTS d_tag_id
CONSTANTS d_default_domain
(* Override in extending model *)
ProcessEnabled( stepdefs, s ) == FALSE
ProcessRunning( stepdefs ) == {} \* Head( stepdefs )
ProcessParameter( stepdefs ) == {} \* Head( stepdefs )
ProcessesToRun( stepdefs ) == {} \* Tail( stepdefs )
TickNext( t ) == t + 1 \* advance time (when process start)
(******************************************************************
Initial value for infrastructure service responses
- modelData infrastructureServices
- template infrastructure-service-init.mustache
******************************************************************)
\* create record to put into 'responses'variable field
InfrastructureServiceResponse( status, response ) == [ status |-> status, response |-> response ]
\* Initial value to variable 'responses'
InfrastructureServiceInit == [ p__sf_lead_post_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_account_post_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_account_get_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_lead_get_ |-> InfrastructureServiceResponse( Nil, Nil ) ]
(******************************************************************
Defined types Data type definitions
- modelData definitions
- template definition_types.mustache
*******************************************************************)
t_Status == [
code: d_default_domain,
message: d_default_domain
] \* definition 'Status'
t_Lead == [
id: d_lead_id,
name: d_name,
street: d_street,
city: d_city
] \* definition 'Lead'
t_Address == [
street: d_street,
city: d_city
] \* definition 'Address'
t_Owner == [
name: d_name,
address: t_Address
] \* definition 'Owner'
t_Tag == [
id: d_tag_id,
account_id: d_account_id,
owner: t_Owner
] \* definition 'Tag'
t_salesf_Lead == [
Id: d_lead_id,
IsDeleted: d_not_used,
MasterRecordId: d_not_used,
LastName: d_not_used,
FirstName: d_not_used,
Salutation: d_not_used,
Name: d_name,
Title: d_not_used,
Company: d_not_used,
Street: d_street,
City: d_city,
State: d_not_used,
PostalCode: d_not_used,
Country: d_not_used,
Latitude: d_not_used,
Longitude: d_not_used,
Address: d_not_used,
Phone: d_not_used,
MobilePhone: d_not_used,
Fax: d_not_used,
Email: d_not_used,
Website: d_not_used,
PhotoUrl: d_not_used,
Description: d_not_used,
LeadSource: d_not_used,
Status: d_not_used,
Industry: d_not_used,
Rating: d_not_used,
AnnualRevenue: d_not_used,
NumberOfEmployees: d_not_used,
OwnerId: d_not_used,
IsConverted: d_not_used,
ConvertedDate: d_not_used,
ConvertedAccountId: d_not_used,
ConvertedContactId: d_not_used,
ConvertedOpportunityId: d_not_used,
IsUnreadByOwner: d_not_used,
CreatedDate: d_not_used,
CreatedById: d_not_used,
LastModifiedDate: d_not_used,
LastModifiedById: d_not_used,
SystemModstamp: d_not_used,
LastActivityDate: d_not_used,
LastViewedDate: d_not_used,
LastReferencedDate: d_not_used,
Jigsaw: d_not_used,
JigsawContactId: d_not_used,
CleanStatus: d_not_used,
CompanyDunsNumber: d_not_used,
DandbCompanyId: d_not_used,
EmailBouncedReason: d_not_used,
EmailBouncedDate: d_not_used,
SICCode__c: d_not_used,
ProductInterest__c: d_not_used,
Primary__c: d_not_used,
CurrentGenerators__c: d_not_used,
NumberofLocations__c: d_not_used,
pet_tag__c: d_not_used
] \* definition 'salesf_Lead'
t_salesf_Account == [
Id: d_account_id,
IsDeleted: d_not_used,
MasterRecordId: d_not_used,
Name: d_name,
Type: d_not_used,
ParentId: d_not_used,
BillingStreet: d_not_used,
BillingCity: d_not_used,
BillingState: d_not_used,
BillingPostalCode: d_not_used,
BillingCountry: d_not_used,
BillingLatitude: d_not_used,
BillingLongitude: d_not_used,
BillingAddress: d_not_used,
ShippingStreet: d_not_used,
ShippingCity: d_not_used,
ShippingState: d_not_used,
ShippingPostalCode: d_not_used,
ShippingCountry: d_not_used,
ShippingLatitude: d_not_used,
ShippingLongitude: d_not_used,
ShippingAddress: d_not_used,
Phone: d_not_used,
Fax: d_not_used,
AccountNumber: d_not_used,
Website: d_not_used,
PhotoUrl: d_not_used,
Sic: d_not_used,
Industry: d_not_used,
AnnualRevenue: d_not_used,
NumberOfEmployees: d_not_used,
Ownership: d_not_used,
TickerSymbol: d_not_used,
Description: d_not_used,
Rating: d_not_used,
Site: d_not_used,
OwnerId: d_not_used,
CreatedDate: d_not_used,
CreatedById: d_not_used,
LastModifiedDate: d_not_used,
LastModifiedById: d_not_used,
SystemModstamp: d_not_used,
LastActivityDate: d_not_used,
LastViewedDate: d_not_used,
LastReferencedDate: d_not_used,
Jigsaw: d_not_used,
JigsawCompanyId: d_not_used,
CleanStatus: d_not_used,
AccountSource: d_not_used,
DunsNumber: d_not_used,
Tradestyle: d_not_used,
NaicsCode: d_not_used,
NaicsDesc: d_not_used,
YearStarted: d_not_used,
SicDesc: d_not_used,
DandbCompanyId: d_not_used,
CustomerPriority__c: d_not_used,
SLA__c: d_not_used,
Active__c: d_not_used,
NumberofLocations__c: d_not_used,
UpsellOpportunity__c: d_not_used,
SLASerialNumber__c: d_not_used,
SLAExpirationDate__c: d_not_used,
jj_added_me__c: d_not_used,
pet_tag__c: d_not_used
] \* definition 'salesf_Account'
(******************************************************************
Interface input types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
t__usecase_generate_lead_post_ == [
lead: t_salesf_Lead
] \* operation '/usecase/generate_lead(post)' --> process 'p__usecase_generate_lead_post_'
t__usecase_create_account_post_ == [
account: t_salesf_Account
] \* operation '/usecase/create_account(post)' --> process 'p__usecase_create_account_post_'
t__usecase_prepare_blank_tag_post_ == [dummy: {Nil}
] \* operation '/usecase/prepare_blank_tag(post)' --> process 'p__usecase_prepare_blank_tag_post_'
t__usecase_register_tag_post_ == [
tag_id: d_default_domain,
lead_id: d_default_domain,
account_id: d_default_domain,
owners: t_Owner
] \* operation '/usecase/register_tag(post)' --> process 'p__usecase_register_tag_post_'
\* end of Interface input types
(******************************************************************
Interface response types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
t_resp__usecase_generate_lead_post_ ==[
status_default: t_Status
] \* interface '_usecase_generate_lead_post_' response type
t_resp__usecase_create_account_post_ ==[
status_default: t_Status
] \* interface '_usecase_create_account_post_' response type
t_resp__usecase_prepare_blank_tag_post_ ==[
status_200: t_Tag,
status_default: t_Status
] \* interface '_usecase_prepare_blank_tag_post_' response type
t_resp__usecase_register_tag_post_ ==[
status_200: t_Tag,
status_default: t_Status
] \* interface '_usecase_register_tag_post_' response type
(*
--algorithm model {
(******************************************************************
State environment model
- modelData none
- template tla/plc_run_state.mustache
******************************************************************)
variables
steps = Steps; \* sequence of [ { process |-> {}, parameter |-> {} }]
step = Nil; \* processes currently enabled
step_parameter = {}; \* paramter binding for currently enabled processes
now = 0; \* current time
(******************************************************************
Variables used by infrastructure-services
- modelData none
- template infrastructure-service-variables.mustache
******************************************************************)
\* Variable for returning responses from infrastructure services
responses = InfrastructureServiceInit;
(*
Extension point for specification state
- modelData none
- template extend/extend_state.mustache
*)
\* Salesforce
\* accounts in Salesforce, type t_salesf_LeadPet, initially empty
v_Accounts = {};
\* leads in Salesforce, type t_salesf_LeadPet, initially empty
v_Leads = {};
\* Petstore ERP
\* tags in Petstore ERP, type t_Tag, initially empty
v_Tags = {};
\* ID generators
\* Valid ids a re all domain elements except 'Nil'
v_tag_ids = d_tag_id \ {Nil}
(******************************************************************
State varibles: Specification state
- modelData variables
- template state_variables.mustache
******************************************************************)
define {
(*
Current time in state variable now gets ticked
when process starts.
*)
currentTime == now
(*
Variable step_parameter' contains a record with field 'bindSet', which
contains a set with input for the process. If 'bindSet' is 'Nil' return
whole 'inputSet'
*)
ProcessParameterInput( inputSet ) == IF (CHOOSE s \in step_parameter': TRUE).bindSet = Nil
THEN inputSet
ELSE (CHOOSE s \in step_parameter': TRUE).bindSet
(* All record fields in 'bindDef' must bind with corresponding fields in 'inputParam' *)
\* ProcessParameterEnablesTst( inputParam, bindDefs ) == \A key \in { k \in DOMAIN bindDefs : k # "_key" }: bindDefs[key] = inputParam[key]
(*
ProcessParameterEnables: 'inputParam' satisfies 'bindDefs'
- all 'normal' field in 'bindDefs' are found in 'inputParam'
- and all subrecords can be validated recursively using 'ProcessParameterEnables' using a the set in field '_key'
- and each record in the set in field '_rows' validates at least one row in 'inputParam'
-- cardinality of inputParam[key] = cardinality _row.set
Recurse one level down in 'inputParam' using keys 'bindDefs._key.key'.
Recursion is done only if 'bindDefs' defines field '_key'.
Should be implemented using recursion, but at the time of writing this comment could not make it work.
*)
RECURSIVE ProcessParameterEnables( _, _ )
ProcessParameterEnables( inputParam, bindDefs ) == ( \A key \in { k \in DOMAIN bindDefs : k # "_key" /\ k # "_rows" }: bindDefs[key] = inputParam[key] )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_key" }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\ \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef )
)
(* ProcessParameterBind operator
Bind 'inputParam' for the process currently being executed with values in 'step_parameter'.
Bind to inputParameter allowed if one the following matches
- step parameter WildCard
- process parameter = WildCard
- predicate 'ProcessParameterEnables' resolves TRUE for some paramter set in 'step_parameter'
*)
ProcessParameterBind( inputParam ) == step_parameter' = WildCard
\/ { processEnabledInStep \in step_parameter' :
processEnabledInStep.process = step'
/\ ( processEnabledInStep.bindRule = WildCard
\/ ProcessParameterEnables( inputParam, processEnabledInStep.bindRule ) ) } # {}
(******************************************************************
Operators for infrastrcuture service (generated)
- modelData infrastructureServices
- template operator-infrastructure-service.mustache
******************************************************************)
InterfaceOperation2ProcessName( op ) == CASE op = "xxXXxx" -> Nil
[] op = "/sf/lead(post)" -> "p__sf_lead_post_"
[] op = "/sf/account(post)" -> "p__sf_account_post_"
[] op = "/sf/account(get)" -> "p__sf_account_get_"
[] op = "/sf/lead(get)" -> "p__sf_lead_get_"
[] OTHER -> Assert( FALSE, "Unknown infrastructure service" )
(******************************************************************
Operators supporting infrastructure services
- modelData none
- template tla/operators-infrastructure-service.mustache
******************************************************************)
\* return response for 'operation' from 'responses' state variable
InfrastructureServiceGetResponse( operation ) == responses[InterfaceOperation2ProcessName(operation)].response
\* return status for 'operation' from 'responses' state variable
InfrastructureServiceGetStatus( operation ) == responses[InterfaceOperation2ProcessName(operation)].status
(*
Extension point for operations
- modelData none
- template extend/extend_operations.mustache
*)
\* All fields on a lead mandatory
ValidLead( lead ) == \A key \in { "Id", "Name" }: lead[key] # Nil
\* All fields on a lead mandatory
ValidAccount( account ) == \A key \in { "Id"}: account[key] # Nil
New_Empty_Address == [ key \in DOMAIN CHOOSE x \in t_Address: TRUE |-> Nil ]
New_Empty_Owner == [ name |-> Nil, address |-> New_Empty_Address ]
\* Create new empty tag identiefied by 'id'
New_Empty_Tag( id ) == [ id |-> id,
account_id |-> Nil,
owner |-> New_Empty_Owner
]\* Take one id from the set of tag identifiers initialized in `v_tag_ids`
Next_Tag_id == CHOOSE x \in v_tag_ids: TRUE
} \* define
(***********************************************************************
Macros to control process execution && time
***********************************************************************)
macro tick() {
now := TickNext( now ); \* now := now + 1;
}
macro enable( s ) {
(* head in sequence 'steps' enable processes *)
\* await Len( steps ) # 0 /\ ProcessEnabled( steps, s );
await ProcessEnabled( steps, s );
(* process entered, remove head from sequence 'steps' *)
step := ProcessRunning( steps ); \* Head( steps );
step_parameter := ProcessParameter( steps );
\* steps := ProcessesToRun( steps ); \* Tail( steps );
(* Reset infrastructure service responses on process entry *)
responses := InfrastructureServiceInit;
(* time advances by one tick for each process step *)
tick();
\* debug( s );
}
(* Remove currently running prosess from head of 'step'.
Calling this macro enables next process to take turn.
If a process comprises several steps, this results
processes runing parallel, unless 'process_done' is
called in the end of the process.
*)
macro process_done( s ) {
steps := ProcessesToRun( steps ); \* Tail( steps );
}
(******************************************************************
Macros for infrastructure services
- modelData none
- template tla/macro-infrastructure-service.mustache
******************************************************************)
\* set 'status' with 'response' for 'operation' into state variable 'responses'
macro InfrastructureServiceReturn( operation, status, response ) {
\* update field for 'operation' in 'responses' variable with record [ status |-> s , response |-> r ]
responses[InterfaceOperation2ProcessName(operation)] := InfrastructureServiceResponse( status, response );
}
(*
Extension poin to add macros
- modelData none
- template extend/extend_macros.mustache
*)
(* ******************************************************************
Transactions (modify state)
* ******************************************************************)
macro lead_enter( lead ) {
v_Leads := { entry \in v_Leads: entry.Id # lead.Id } \union { lead };
}
macro account_enter( account ) {
v_Accounts := { entry \in v_Accounts: entry.Id # account.Id } \union { account };
}
macro tag_enter( tag ) {
v_Tags := v_Tags \union {tag};
}
(*
* @param id [d_tag_id] next free tag id generated
*)
macro next_tag_id( id ) {
\* 'id' must be free
assert( id \in v_tag_ids );
\* consume it - it not free any more
v_tag_ids := v_tag_ids \ { id };
}
(* ******************************************************************
Macros implmeneting entries to interface services
* ******************************************************************)
\* Interface macro implementing entry for service 'generate_lead(post)'
macro uc_generate_lead( input ) {
\* passed directory to salesforce
call salesforce_lead_post( input.lead );
}
\* Interface macro implementing entry for service 'generate_lead(post)'
macro uc_create_account( input ) {
\* passed directly to salesforce
call salesforce_account_post( input.account );
}
\* Entry for use use case interface /usecase/prepare_blank_tag(post)
\* No input (
macro uc_prepare_blank_tag( input ) {
\* Does no define any input
assert( input = [ dummy |-> Nil ] );
\* Implementation in Petstore ERP
call petstore_prepare_blank_tag();
}
macro uc_register_tag( input ) {
call petstore_register_tag( input );
}
(******************************************************************
Interfaces generated Create a dummy procedure to have 'defaultInitValue' in the model
- modelData none
- template interface_stubs_dummy.mustache
******************************************************************)
(* Allow 'interface-extension.implementation' without specification code snippet *)
macro dummy( dummy_input ) {
print << "Dummy macro called should replace with actual macro" >>;
}
(* Create a dummy procedure with input variable so that pcal creates
constant defaultInitValue (which is assigned a value in setup.tla)
*)
procedure dummy( dummy_input ) {
dummy_start: skip;
}
(*
Extension point for implementation
- modelData none
- template extend/extend_implementation.mustache
*)
\* Salesforce service /sf/lead(post)
procedure salesforce_lead_post( lead ) {
salesforce_lead_post:
\* Correct input typ
assert( lead \in t_salesf_Lead );
\* Validate input data
if ( ~ValidLead( lead ) ) {
InfrastructureServiceReturn( "/sf/lead(post)", "status_404", Nil );
return;
};
\* Input validation passed: enter to database
salesforce_lead_valid_input:
lead_enter( lead );
InfrastructureServiceReturn( "/sf/lead(post)", "status_200", Nil );
return;
}
\* Salesforce service /sf/account(post)
procedure salesforce_account_post( account ) {
salesforce_account_post:
\* Correct input typ
assert( account \in t_salesf_Account );
\* Validate input data
if ( ~ValidAccount( account ) ) {
InfrastructureServiceReturn( "/sf/account(post)", "status_404", Nil );
return;
};
\* Input validation passed: enter to database
salesforce_account_valid_input:
account_enter( account );
InfrastructureServiceReturn( "/sf/account(post)", "status_200", Nil );
return;
}
procedure petstore_prepare_blank_tag( ) {
petstore_prepare_blank_start:
\* Generate next tag id
next_tag_id( Next_Tag_id );
\* Create new tag using tag id
tag_enter( New_Empty_Tag(Next_Tag_id) );
petstore_prepare_blank_done:
return;
}
procedure petstore_register_tag( input ) {
petstore_register_tag_start:
print << "input:", input >>;
\* Implementation in Petstore ERP
call petstore_prepare_blank_tag();
petstore_register_tag_done:
return;
}
(******************************************************************
Interfaces generated Process interfaces
- modelData interfaces
- template interface_processes.mustache
******************************************************************)
(* Process /usecase/generate_lead(post) *)
fair process (p__usecase_generate_lead_post_="/usecase/generate_lead(post)") {
p__usecase_generate_lead_post__enter: while (TRUE) {
enable( "p__usecase_generate_lead_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/generate_lead(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_generate_lead_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_generate_lead_post_ for operation '/usecase/generate_lead(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_generate_lead_post_ );
uc_generate_lead( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_generate_lead_post__exit: process_done( "/usecase/generate_lead(post)" );
} \* while(TRUE)
} \* failr process p__usecase_generate_lead_post_
(* Process /usecase/create_account(post) *)
fair process (p__usecase_create_account_post_="/usecase/create_account(post)") {
p__usecase_create_account_post__enter: while (TRUE) {
enable( "p__usecase_create_account_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/create_account(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_create_account_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_create_account_post_ for operation '/usecase/create_account(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_create_account_post_ );
uc_create_account( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_create_account_post__exit: process_done( "/usecase/create_account(post)" );
} \* while(TRUE)
} \* failr process p__usecase_create_account_post_
(* Process /usecase/prepare_blank_tag(post) *)
fair process (p__usecase_prepare_blank_tag_post_="/usecase/prepare_blank_tag(post)") {
p__usecase_prepare_blank_tag_post__enter: while (TRUE) {
enable( "p__usecase_prepare_blank_tag_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/prepare_blank_tag(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_prepare_blank_tag_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_prepare_blank_tag_post_ for operation '/usecase/prepare_blank_tag(post)',tick=", currentTime>>;
(* Valid input type? - API configuration did not define any parameters - must have Nil for _input.dummy: *)
assert( _input.dummy = Nil );
uc_prepare_blank_tag( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_prepare_blank_tag_post__exit: process_done( "/usecase/prepare_blank_tag(post)" );
} \* while(TRUE)
} \* failr process p__usecase_prepare_blank_tag_post_
(* Process /usecase/register_tag(post) *)
fair process (p__usecase_register_tag_post_="/usecase/register_tag(post)") {
p__usecase_register_tag_post__enter: while (TRUE) {
enable( "p__usecase_register_tag_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/register_tag(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_register_tag_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_register_tag_post_ for operation '/usecase/register_tag(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_register_tag_post_ );
uc_register_tag( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_register_tag_post__exit: process_done( "/usecase/register_tag(post)" );
} \* while(TRUE)
} \* failr process p__usecase_register_tag_post_
fair process ( tail="Tail") {
tail_wait: await( Len(steps) = 0 );
step := "Tail";
step_parameter := {};
tail: while( TRUE ) {
skip;
}
}
} \* end of algorithm
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
(******************************************************************
Type invariants: Type constraint in specification
- modelData variables
- template state_type_invariant.mustache
******************************************************************)
(******************************************************************
Validate types for infrastructure service return values
- modelData infrastructureServices
- template state_type_invariant-infrastructure-service.mustache
******************************************************************)
(*
Type invariants for infrastructure service return values.
All fields in 'responses' state variable store a record [ status |-> ... , response |-> ... ]
*)
InfrastructureService_TypeInvariant__sf_lead_post_ == responses.p__sf_lead_post_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_account_post_ == responses.p__sf_account_post_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_account_get_ == responses.p__sf_account_get_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_lead_get_ == responses.p__sf_lead_get_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant == TRUE
/\ InfrastructureService_TypeInvariant__sf_lead_post_
/\ InfrastructureService_TypeInvariant__sf_account_post_
/\ InfrastructureService_TypeInvariant__sf_account_get_
/\ InfrastructureService_TypeInvariant__sf_lead_get_
(*
Extension point for specification invariants
- modelData none
- template extend/extend_invariant.mustache
*)
\* Operators for correctness
\* Type constraints
Leads_TypeInvariant == \A entry \in v_Leads: entry \in t_salesf_Lead
Account_TypeInvariant == \A entry \in v_Accounts: entry \in t_salesf_Account
Tag_TypeInvariant == \A entry \in v_Tags: entry \in t_Tag
\* Correcness criteria
\* All entries in state variable 'v_Leads' are 'ValidLead'
Correctness_lead_valid == \A entry \in v_Leads: ValidLead( entry )
\* All entries in 'v_Leads' have unique 'id'
Correctness_lead_unique == \A lead1 \in v_Leads: \A lead2 \in v_Leads: lead1.Id = lead2.Id => lead1 = lead2
\* Combine all correcness criteria on 'Lead', this operator confiugered as INVARIANT
Correctness_lead ==
Correctness_lead_valid
/\ Correctness_lead_unique
\* All entries in state variable 'v_Accounts' are 'ValidAccount'
Correctness_account_valid == \A entry \in v_Accounts: ValidAccount( entry )
\* All entries in 'v_Accounts' have unique 'id'
Correctness_account_unique == \A account1 \in v_Accounts: \A account2 \in v_Accounts: account1.Id = account2.Id => account1 = account2
\* Combine all correcness criteria on 'Account', this operator confiugered as INVARIANT
Correctness_account ==
Correctness_account_valid
/\ Correctness_account_unique
\* Operators for possibilities
(*
Define an operator 'at_least_two_tags' to check that
at least two entries are found in state variable 'v_tags'.
*)
at_least_two_leads == Cardinality( v_Leads ) > 1
(*
Possibility operator to check that at least two entries are found
in state variable 'v_Tags'.
*)
at_least_two_tags == Cardinality( v_Tags ) > 1
at_least_two_accounts == Cardinality( v_Accounts ) > 1
(*
Extension point for assumptions
- modelData none
- template extend/extend_assumptions.mustache
*)
(* ******************************************************************
Helpers to make assumptions
******************************************************************)
(*
True iff in all records in 'set' have 'field' type 'domain'
Cannot evaluate 'p \in set' if set contains too many elements
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in set } = domain
Attempted to construct a set with too many elements (>1000000).
Assume_CorrectDomain( set, field, domain ) == (CHOOSE x \in set : TRUE)[field] \in domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == set[field] = domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == DOMAIN set[field] = domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == (CHOOSE x \in set[field] : TRUE) \in domain
Overflow when computing the number of elements in:
Assume_CorrectDomain( set, field, domain ) == IF Cardinality( set ) > 100
THEN Print( << "Set cardinality exceeded ", Cardinality( set ), " continue" >>, TRUE )
ELSE { p[field] : p \in set } = domain
*)
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in set } = domain
Assume_salesf_Lead_Domains ==
Assume_CorrectDomain( t_salesf_Lead, "Id", d_lead_id )
/\ Assume_CorrectDomain( t_salesf_Lead, "Name", d_name )
/\ Assume_CorrectDomain( t_salesf_Lead, "Street", d_street )
/\ Assume_CorrectDomain( t_salesf_Lead, "City", d_city )
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
ASSUME Assume_salesf_Lead_Domains
Assume_salesf_Account_Domains ==
Assume_CorrectDomain( t_salesf_Account, "Id", d_account_id )
/\ Assume_CorrectDomain( t_salesf_Account, "Name", d_name )
/\ Assume_CorrectDomain( t_salesf_Account, "Street", d_street )
/\ Assume_CorrectDomain( t_salesf_Account, "City", d_city )
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
\* ASSUME Assume_salesf_Account_Domains
Assume_Lead_Domains ==
Assume_CorrectDomain( t_Lead, "id", d_lead_id )
ASSUME Assume_Lead_Domains
Assume_Tag_Domains ==
Assume_CorrectDomain( t_Tag, "id", d_tag_id )
ASSUME Assume_Tag_Domains
Assume_Address_Domains ==
Assume_CorrectDomain( t_Address, "street", d_street )
/\ Assume_CorrectDomain( t_Address, "city", d_city )
ASSUME Assume_Address_Domains
Assume_Owner_Domains ==
Assume_CorrectDomain( t_Owner, "name", d_name )
ASSUME Assume_Owner_Domains
=============================================================================
Raw
model.tla
Model version: 0.0.1-SNAPSHOT
Generator version: 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
------------------------------ MODULE model ------------------------------
EXTENDS TLC, FiniteSets, Sequences, Naturals
(* Execution environment *)
CONSTANTS Steps \* Sequence process/parameter records
(* Magic values *)
CONSTANTS WildCard \* bind to any value
CONSTANTS Nil \* no value
(******************************************************************
Extension point for constants
- modelData none
- template extend/extend_const.mustache
******************************************************************)
(******************************************************************
Domain definitions
- modelData domains
- template domains.mustache
******************************************************************)
CONSTANTS d_name
CONSTANTS d_street
CONSTANTS d_city
CONSTANTS d_lead_id
CONSTANTS d_not_used
CONSTANTS d_account_id
CONSTANTS d_tag_id
CONSTANTS d_default_domain
(* Override in extending model *)
ProcessEnabled( stepdefs, s ) == FALSE
ProcessRunning( stepdefs ) == {} \* Head( stepdefs )
ProcessParameter( stepdefs ) == {} \* Head( stepdefs )
ProcessesToRun( stepdefs ) == {} \* Tail( stepdefs )
TickNext( t ) == t + 1 \* advance time (when process start)
(******************************************************************
Initial value for infrastructure service responses
- modelData infrastructureServices
- template infrastructure-service-init.mustache
******************************************************************)
\* create record to put into 'responses'variable field
InfrastructureServiceResponse( status, response ) == [ status |-> status, response |-> response ]
\* Initial value to variable 'responses'
InfrastructureServiceInit == [ p__sf_lead_post_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_account_post_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_account_get_ |-> InfrastructureServiceResponse( Nil, Nil ), p__sf_lead_get_ |-> InfrastructureServiceResponse( Nil, Nil ) ]
(******************************************************************
Defined types Data type definitions
- modelData definitions
- template definition_types.mustache
*******************************************************************)
t_Status == [
code: d_default_domain,
message: d_default_domain
] \* definition 'Status'
t_Lead == [
id: d_lead_id,
name: d_name,
street: d_street,
city: d_city
] \* definition 'Lead'
t_Address == [
street: d_street,
city: d_city
] \* definition 'Address'
t_Owner == [
name: d_name,
address: t_Address
] \* definition 'Owner'
t_Tag == [
id: d_tag_id,
account_id: d_account_id,
owner: t_Owner
] \* definition 'Tag'
t_salesf_Lead == [
Id: d_lead_id,
IsDeleted: d_not_used,
MasterRecordId: d_not_used,
LastName: d_not_used,
FirstName: d_not_used,
Salutation: d_not_used,
Name: d_name,
Title: d_not_used,
Company: d_not_used,
Street: d_street,
City: d_city,
State: d_not_used,
PostalCode: d_not_used,
Country: d_not_used,
Latitude: d_not_used,
Longitude: d_not_used,
Address: d_not_used,
Phone: d_not_used,
MobilePhone: d_not_used,
Fax: d_not_used,
Email: d_not_used,
Website: d_not_used,
PhotoUrl: d_not_used,
Description: d_not_used,
LeadSource: d_not_used,
Status: d_not_used,
Industry: d_not_used,
Rating: d_not_used,
AnnualRevenue: d_not_used,
NumberOfEmployees: d_not_used,
OwnerId: d_not_used,
IsConverted: d_not_used,
ConvertedDate: d_not_used,
ConvertedAccountId: d_not_used,
ConvertedContactId: d_not_used,
ConvertedOpportunityId: d_not_used,
IsUnreadByOwner: d_not_used,
CreatedDate: d_not_used,
CreatedById: d_not_used,
LastModifiedDate: d_not_used,
LastModifiedById: d_not_used,
SystemModstamp: d_not_used,
LastActivityDate: d_not_used,
LastViewedDate: d_not_used,
LastReferencedDate: d_not_used,
Jigsaw: d_not_used,
JigsawContactId: d_not_used,
CleanStatus: d_not_used,
CompanyDunsNumber: d_not_used,
DandbCompanyId: d_not_used,
EmailBouncedReason: d_not_used,
EmailBouncedDate: d_not_used,
SICCode__c: d_not_used,
ProductInterest__c: d_not_used,
Primary__c: d_not_used,
CurrentGenerators__c: d_not_used,
NumberofLocations__c: d_not_used,
pet_tag__c: d_not_used
] \* definition 'salesf_Lead'
t_salesf_Account == [
Id: d_account_id,
IsDeleted: d_not_used,
MasterRecordId: d_not_used,
Name: d_name,
Type: d_not_used,
ParentId: d_not_used,
BillingStreet: d_not_used,
BillingCity: d_not_used,
BillingState: d_not_used,
BillingPostalCode: d_not_used,
BillingCountry: d_not_used,
BillingLatitude: d_not_used,
BillingLongitude: d_not_used,
BillingAddress: d_not_used,
ShippingStreet: d_not_used,
ShippingCity: d_not_used,
ShippingState: d_not_used,
ShippingPostalCode: d_not_used,
ShippingCountry: d_not_used,
ShippingLatitude: d_not_used,
ShippingLongitude: d_not_used,
ShippingAddress: d_not_used,
Phone: d_not_used,
Fax: d_not_used,
AccountNumber: d_not_used,
Website: d_not_used,
PhotoUrl: d_not_used,
Sic: d_not_used,
Industry: d_not_used,
AnnualRevenue: d_not_used,
NumberOfEmployees: d_not_used,
Ownership: d_not_used,
TickerSymbol: d_not_used,
Description: d_not_used,
Rating: d_not_used,
Site: d_not_used,
OwnerId: d_not_used,
CreatedDate: d_not_used,
CreatedById: d_not_used,
LastModifiedDate: d_not_used,
LastModifiedById: d_not_used,
SystemModstamp: d_not_used,
LastActivityDate: d_not_used,
LastViewedDate: d_not_used,
LastReferencedDate: d_not_used,
Jigsaw: d_not_used,
JigsawCompanyId: d_not_used,
CleanStatus: d_not_used,
AccountSource: d_not_used,
DunsNumber: d_not_used,
Tradestyle: d_not_used,
NaicsCode: d_not_used,
NaicsDesc: d_not_used,
YearStarted: d_not_used,
SicDesc: d_not_used,
DandbCompanyId: d_not_used,
CustomerPriority__c: d_not_used,
SLA__c: d_not_used,
Active__c: d_not_used,
NumberofLocations__c: d_not_used,
UpsellOpportunity__c: d_not_used,
SLASerialNumber__c: d_not_used,
SLAExpirationDate__c: d_not_used,
jj_added_me__c: d_not_used,
pet_tag__c: d_not_used
] \* definition 'salesf_Account'
(******************************************************************
Interface input types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
t__usecase_generate_lead_post_ == [
lead: t_salesf_Lead
] \* operation '/usecase/generate_lead(post)' --> process 'p__usecase_generate_lead_post_'
t__usecase_create_account_post_ == [
account: t_salesf_Account
] \* operation '/usecase/create_account(post)' --> process 'p__usecase_create_account_post_'
t__usecase_prepare_blank_tag_post_ == [dummy: {Nil}
] \* operation '/usecase/prepare_blank_tag(post)' --> process 'p__usecase_prepare_blank_tag_post_'
t__usecase_register_tag_post_ == [
tag_id: d_default_domain,
lead_id: d_default_domain,
account_id: d_default_domain,
owners: t_Owner
] \* operation '/usecase/register_tag(post)' --> process 'p__usecase_register_tag_post_'
\* end of Interface input types
(******************************************************************
Interface response types: Interface types
- modelData interfaces
- template interface_types.mustache
*******************************************************************)
t_resp__usecase_generate_lead_post_ ==[
status_default: t_Status
] \* interface '_usecase_generate_lead_post_' response type
t_resp__usecase_create_account_post_ ==[
status_default: t_Status
] \* interface '_usecase_create_account_post_' response type
t_resp__usecase_prepare_blank_tag_post_ ==[
status_200: t_Tag,
status_default: t_Status
] \* interface '_usecase_prepare_blank_tag_post_' response type
t_resp__usecase_register_tag_post_ ==[
status_200: t_Tag,
status_default: t_Status
] \* interface '_usecase_register_tag_post_' response type
(*
--algorithm model {
(******************************************************************
State environment model
- modelData none
- template tla/plc_run_state.mustache
******************************************************************)
variables
steps = Steps; \* sequence of [ { process |-> {}, parameter |-> {} }]
step = Nil; \* processes currently enabled
step_parameter = {}; \* paramter binding for currently enabled processes
now = 0; \* current time
(******************************************************************
Variables used by infrastructure-services
- modelData none
- template infrastructure-service-variables.mustache
******************************************************************)
\* Variable for returning responses from infrastructure services
responses = InfrastructureServiceInit;
(*
Extension point for specification state
- modelData none
- template extend/extend_state.mustache
*)
\* Salesforce
\* accounts in Salesforce, type t_salesf_LeadPet, initially empty
v_Accounts = {};
\* leads in Salesforce, type t_salesf_LeadPet, initially empty
v_Leads = {};
\* Petstore ERP
\* tags in Petstore ERP, type t_Tag, initially empty
v_Tags = {};
\* ID generators
\* Valid ids a re all domain elements except 'Nil'
v_tag_ids = d_tag_id \ {Nil}
(******************************************************************
State varibles: Specification state
- modelData variables
- template state_variables.mustache
******************************************************************)
define {
(*
Current time in state variable now gets ticked
when process starts.
*)
currentTime == now
(*
Variable step_parameter' contains a record with field 'bindSet', which
contains a set with input for the process. If 'bindSet' is 'Nil' return
whole 'inputSet'
*)
ProcessParameterInput( inputSet ) == IF (CHOOSE s \in step_parameter': TRUE).bindSet = Nil
THEN inputSet
ELSE (CHOOSE s \in step_parameter': TRUE).bindSet
(* All record fields in 'bindDef' must bind with corresponding fields in 'inputParam' *)
\* ProcessParameterEnablesTst( inputParam, bindDefs ) == \A key \in { k \in DOMAIN bindDefs : k # "_key" }: bindDefs[key] = inputParam[key]
(*
ProcessParameterEnables: 'inputParam' satisfies 'bindDefs'
- all 'normal' field in 'bindDefs' are found in 'inputParam'
- and all subrecords can be validated recursively using 'ProcessParameterEnables' using a the set in field '_key'
- and each record in the set in field '_rows' validates at least one row in 'inputParam'
-- cardinality of inputParam[key] = cardinality _row.set
Recurse one level down in 'inputParam' using keys 'bindDefs._key.key'.
Recursion is done only if 'bindDefs' defines field '_key'.
Should be implemented using recursion, but at the time of writing this comment could not make it work.
*)
RECURSIVE ProcessParameterEnables( _, _ )
ProcessParameterEnables( inputParam, bindDefs ) == ( \A key \in { k \in DOMAIN bindDefs : k # "_key" /\ k # "_rows" }: bindDefs[key] = inputParam[key] )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_key" }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\ \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef )
)
(* ProcessParameterBind operator
Bind 'inputParam' for the process currently being executed with values in 'step_parameter'.
Bind to inputParameter allowed if one the following matches
- step parameter WildCard
- process parameter = WildCard
- predicate 'ProcessParameterEnables' resolves TRUE for some paramter set in 'step_parameter'
*)
ProcessParameterBind( inputParam ) == step_parameter' = WildCard
\/ { processEnabledInStep \in step_parameter' :
processEnabledInStep.process = step'
/\ ( processEnabledInStep.bindRule = WildCard
\/ ProcessParameterEnables( inputParam, processEnabledInStep.bindRule ) ) } # {}
(******************************************************************
Operators for infrastrcuture service (generated)
- modelData infrastructureServices
- template operator-infrastructure-service.mustache
******************************************************************)
InterfaceOperation2ProcessName( op ) == CASE op = "xxXXxx" -> Nil
[] op = "/sf/lead(post)" -> "p__sf_lead_post_"
[] op = "/sf/account(post)" -> "p__sf_account_post_"
[] op = "/sf/account(get)" -> "p__sf_account_get_"
[] op = "/sf/lead(get)" -> "p__sf_lead_get_"
[] OTHER -> Assert( FALSE, "Unknown infrastructure service" )
(******************************************************************
Operators supporting infrastructure services
- modelData none
- template tla/operators-infrastructure-service.mustache
******************************************************************)
\* return response for 'operation' from 'responses' state variable
InfrastructureServiceGetResponse( operation ) == responses[InterfaceOperation2ProcessName(operation)].response
\* return status for 'operation' from 'responses' state variable
InfrastructureServiceGetStatus( operation ) == responses[InterfaceOperation2ProcessName(operation)].status
(*
Extension point for operations
- modelData none
- template extend/extend_operations.mustache
*)
\* All fields on a lead mandatory
ValidLead( lead ) == \A key \in { "Id", "Name" }: lead[key] # Nil
\* All fields on a lead mandatory
ValidAccount( account ) == \A key \in { "Id"}: account[key] # Nil
New_Empty_Address == [ key \in DOMAIN CHOOSE x \in t_Address: TRUE |-> Nil ]
New_Empty_Owner == [ name |-> Nil, address |-> New_Empty_Address ]
\* Create new empty tag identiefied by 'id'
New_Empty_Tag( id ) == [ id |-> id,
account_id |-> Nil,
owner |-> New_Empty_Owner
]\* Take one id from the set of tag identifiers initialized in `v_tag_ids`
Next_Tag_id == CHOOSE x \in v_tag_ids: TRUE
} \* define
(***********************************************************************
Macros to control process execution && time
***********************************************************************)
macro tick() {
now := TickNext( now ); \* now := now + 1;
}
macro enable( s ) {
(* head in sequence 'steps' enable processes *)
\* await Len( steps ) # 0 /\ ProcessEnabled( steps, s );
await ProcessEnabled( steps, s );
(* process entered, remove head from sequence 'steps' *)
step := ProcessRunning( steps ); \* Head( steps );
step_parameter := ProcessParameter( steps );
\* steps := ProcessesToRun( steps ); \* Tail( steps );
(* Reset infrastructure service responses on process entry *)
responses := InfrastructureServiceInit;
(* time advances by one tick for each process step *)
tick();
\* debug( s );
}
(* Remove currently running prosess from head of 'step'.
Calling this macro enables next process to take turn.
If a process comprises several steps, this results
processes runing parallel, unless 'process_done' is
called in the end of the process.
*)
macro process_done( s ) {
steps := ProcessesToRun( steps ); \* Tail( steps );
}
(******************************************************************
Macros for infrastructure services
- modelData none
- template tla/macro-infrastructure-service.mustache
******************************************************************)
\* set 'status' with 'response' for 'operation' into state variable 'responses'
macro InfrastructureServiceReturn( operation, status, response ) {
\* update field for 'operation' in 'responses' variable with record [ status |-> s , response |-> r ]
responses[InterfaceOperation2ProcessName(operation)] := InfrastructureServiceResponse( status, response );
}
(*
Extension poin to add macros
- modelData none
- template extend/extend_macros.mustache
*)
(* ******************************************************************
Transactions (modify state)
* ******************************************************************)
macro lead_enter( lead ) {
v_Leads := { entry \in v_Leads: entry.Id # lead.Id } \union { lead };
}
macro account_enter( account ) {
v_Accounts := { entry \in v_Accounts: entry.Id # account.Id } \union { account };
}
macro tag_enter( tag ) {
v_Tags := v_Tags \union {tag};
}
(*
* @param id [d_tag_id] next free tag id generated
*)
macro next_tag_id( id ) {
\* 'id' must be free
assert( id \in v_tag_ids );
\* consume it - it not free any more
v_tag_ids := v_tag_ids \ { id };
}
(* ******************************************************************
Macros implmeneting entries to interface services
* ******************************************************************)
\* Interface macro implementing entry for service 'generate_lead(post)'
macro uc_generate_lead( input ) {
\* passed directory to salesforce
call salesforce_lead_post( input.lead );
}
\* Interface macro implementing entry for service 'generate_lead(post)'
macro uc_create_account( input ) {
\* passed directly to salesforce
call salesforce_account_post( input.account );
}
\* Entry for use use case interface /usecase/prepare_blank_tag(post)
\* No input (
macro uc_prepare_blank_tag( input ) {
\* Does no define any input
assert( input = [ dummy |-> Nil ] );
\* Implementation in Petstore ERP
call petstore_prepare_blank_tag();
}
macro uc_register_tag( input ) {
call petstore_register_tag( input );
}
(******************************************************************
Interfaces generated Create a dummy procedure to have &#39;defaultInitValue&#39; in the model
- modelData none
- template interface_stubs_dummy.mustache
******************************************************************)
(* Allow 'interface-extension.implementation' without specification code snippet *)
macro dummy( dummy_input ) {
print << "Dummy macro called should replace with actual macro" >>;
}
(* Create a dummy procedure with input variable so that pcal creates
constant defaultInitValue (which is assigned a value in setup.tla)
*)
procedure dummy( dummy_input ) {
dummy_start: skip;
}
(*
Extension point for implementation
- modelData none
- template extend/extend_implementation.mustache
*)
\* Salesforce service /sf/lead(post)
procedure salesforce_lead_post( lead ) {
salesforce_lead_post:
\* Correct input typ
assert( lead \in t_salesf_Lead );
\* Validate input data
if ( ~ValidLead( lead ) ) {
InfrastructureServiceReturn( "/sf/lead(post)", "status_404", Nil );
return;
};
\* Input validation passed: enter to database
salesforce_lead_valid_input:
lead_enter( lead );
InfrastructureServiceReturn( "/sf/lead(post)", "status_200", Nil );
return;
}
\* Salesforce service /sf/account(post)
procedure salesforce_account_post( account ) {
salesforce_account_post:
\* Correct input typ
assert( account \in t_salesf_Account );
\* Validate input data
if ( ~ValidAccount( account ) ) {
InfrastructureServiceReturn( "/sf/account(post)", "status_404", Nil );
return;
};
\* Input validation passed: enter to database
salesforce_account_valid_input:
account_enter( account );
InfrastructureServiceReturn( "/sf/account(post)", "status_200", Nil );
return;
}
procedure petstore_prepare_blank_tag( ) {
petstore_prepare_blank_start:
\* Generate next tag id
next_tag_id( Next_Tag_id );
\* Create new tag using tag id
tag_enter( New_Empty_Tag(Next_Tag_id) );
petstore_prepare_blank_done:
return;
}
procedure petstore_register_tag( input ) {
petstore_register_tag_start:
print << "input:", input >>;
\* Implementation in Petstore ERP
call petstore_prepare_blank_tag();
petstore_register_tag_done:
return;
}
(******************************************************************
Interfaces generated Process interfaces
- modelData interfaces
- template interface_processes.mustache
******************************************************************)
(* Process /usecase/generate_lead(post) *)
fair process (p__usecase_generate_lead_post_="/usecase/generate_lead(post)") {
p__usecase_generate_lead_post__enter: while (TRUE) {
enable( "p__usecase_generate_lead_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/generate_lead(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_generate_lead_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_generate_lead_post_ for operation '/usecase/generate_lead(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_generate_lead_post_ );
uc_generate_lead( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_generate_lead_post__exit: process_done( "/usecase/generate_lead(post)" );
} \* while(TRUE)
} \* failr process p__usecase_generate_lead_post_
(* Process /usecase/create_account(post) *)
fair process (p__usecase_create_account_post_="/usecase/create_account(post)") {
p__usecase_create_account_post__enter: while (TRUE) {
enable( "p__usecase_create_account_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/create_account(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_create_account_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_create_account_post_ for operation '/usecase/create_account(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_create_account_post_ );
uc_create_account( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_create_account_post__exit: process_done( "/usecase/create_account(post)" );
} \* while(TRUE)
} \* failr process p__usecase_create_account_post_
(* Process /usecase/prepare_blank_tag(post) *)
fair process (p__usecase_prepare_blank_tag_post_="/usecase/prepare_blank_tag(post)") {
p__usecase_prepare_blank_tag_post__enter: while (TRUE) {
enable( "p__usecase_prepare_blank_tag_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/prepare_blank_tag(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_prepare_blank_tag_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_prepare_blank_tag_post_ for operation '/usecase/prepare_blank_tag(post)',tick=", currentTime>>;
(* Valid input type? - API configuration did not define any parameters - must have Nil for _input.dummy: *)
assert( _input.dummy = Nil );
uc_prepare_blank_tag( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_prepare_blank_tag_post__exit: process_done( "/usecase/prepare_blank_tag(post)" );
} \* while(TRUE)
} \* failr process p__usecase_prepare_blank_tag_post_
(* Process /usecase/register_tag(post) *)
fair process (p__usecase_register_tag_post_="/usecase/register_tag(post)") {
p__usecase_register_tag_post__enter: while (TRUE) {
enable( "p__usecase_register_tag_post_" );
(* enable next process to run parallel *)
\* process_done( "/usecase/register_tag(post)" );
with ( _input \in { t \in ProcessParameterInput( t__usecase_register_tag_post_ ) : ProcessParameterBind( t ) } ) {
\* PREFERENCES.debug-output: true
print <<"Default process p__usecase_register_tag_post_ for operation '/usecase/register_tag(post)',tick=", currentTime>>;
(* Valid input type? - _input must match type of API request *)
assert( _input \in t__usecase_register_tag_post_ );
uc_register_tag( _input );
}; \* with _input
(* enable next process - after current process *)
p__usecase_register_tag_post__exit: process_done( "/usecase/register_tag(post)" );
} \* while(TRUE)
} \* failr process p__usecase_register_tag_post_
fair process ( tail="Tail") {
tail_wait: await( Len(steps) = 0 );
step := "Tail";
step_parameter := {};
tail: while( TRUE ) {
skip;
}
}
} \* end of algorithm
*)
\* BEGIN TRANSLATION
\* Label salesforce_lead_post of procedure salesforce_lead_post at line 614 col 8 changed to salesforce_lead_post_
\* Label salesforce_account_post of procedure salesforce_account_post at line 639 col 8 changed to salesforce_account_post_
\* Label tail of process tail at line 766 col 15 changed to tail_
CONSTANT defaultInitValue
VARIABLES steps, step, step_parameter, now, responses, v_Accounts, v_Leads,
v_Tags, v_tag_ids, pc, stack
(* define statement *)
currentTime == now
ProcessParameterInput( inputSet ) == IF (CHOOSE s \in step_parameter': TRUE).bindSet = Nil
THEN inputSet
ELSE (CHOOSE s \in step_parameter': TRUE).bindSet
RECURSIVE ProcessParameterEnables( _, _ )
ProcessParameterEnables( inputParam, bindDefs ) == ( \A key \in { k \in DOMAIN bindDefs : k # "_key" /\ k # "_rows" }: bindDefs[key] = inputParam[key] )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_key" }: \A r \in bindDefs[reckey] : ProcessParameterEnables( inputParam[r.key], r.rec ) )
/\ ( \A reckey \in { k \in DOMAIN bindDefs : k = "_rows" }: \A r \in bindDefs[reckey] :
Cardinality( r.set ) = Cardinality( inputParam[r.key] ) /\ \A bDef \in r.set: \E ip \in inputParam[r.key]: ProcessParameterEnables( ip, bDef )
)
ProcessParameterBind( inputParam ) == step_parameter' = WildCard
\/ { processEnabledInStep \in step_parameter' :
processEnabledInStep.process = step'
/\ ( processEnabledInStep.bindRule = WildCard
\/ ProcessParameterEnables( inputParam, processEnabledInStep.bindRule ) ) } # {}
InterfaceOperation2ProcessName( op ) == CASE op = "xxXXxx" -> Nil
[] op = "/sf/lead(post)" -> "p__sf_lead_post_"
[] op = "/sf/account(post)" -> "p__sf_account_post_"
[] op = "/sf/account(get)" -> "p__sf_account_get_"
[] op = "/sf/lead(get)" -> "p__sf_lead_get_"
[] OTHER -> Assert( FALSE, "Unknown infrastructure service" )
InfrastructureServiceGetResponse( operation ) == responses[InterfaceOperation2ProcessName(operation)].response
InfrastructureServiceGetStatus( operation ) == responses[InterfaceOperation2ProcessName(operation)].status
ValidLead( lead ) == \A key \in { "Id", "Name" }: lead[key] # Nil
ValidAccount( account ) == \A key \in { "Id"}: account[key] # Nil
New_Empty_Address == [ key \in DOMAIN CHOOSE x \in t_Address: TRUE |-> Nil ]
New_Empty_Owner == [ name |-> Nil, address |-> New_Empty_Address ]
New_Empty_Tag( id ) == [ id |-> id,
account_id |-> Nil,
owner |-> New_Empty_Owner
]
Next_Tag_id == CHOOSE x \in v_tag_ids: TRUE
VARIABLES dummy_input, lead, account, input
vars == << steps, step, step_parameter, now, responses, v_Accounts, v_Leads,
v_Tags, v_tag_ids, pc, stack, dummy_input, lead, account, input >>
ProcSet == {"/usecase/generate_lead(post)"} \cup {"/usecase/create_account(post)"} \cup {"/usecase/prepare_blank_tag(post)"} \cup {"/usecase/register_tag(post)"} \cup {"Tail"}
Init == (* Global variables *)
/\ steps = Steps
/\ step = Nil
/\ step_parameter = {}
/\ now = 0
/\ responses = InfrastructureServiceInit
/\ v_Accounts = {}
/\ v_Leads = {}
/\ v_Tags = {}
/\ v_tag_ids = d_tag_id \ {Nil}
(* Procedure dummy *)
/\ dummy_input = [ self \in ProcSet |-> defaultInitValue]
(* Procedure salesforce_lead_post *)
/\ lead = [ self \in ProcSet |-> defaultInitValue]
(* Procedure salesforce_account_post *)
/\ account = [ self \in ProcSet |-> defaultInitValue]
(* Procedure petstore_register_tag *)
/\ input = [ self \in ProcSet |-> defaultInitValue]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self = "/usecase/generate_lead(post)" -> "p__usecase_generate_lead_post__enter"
[] self = "/usecase/create_account(post)" -> "p__usecase_create_account_post__enter"
[] self = "/usecase/prepare_blank_tag(post)" -> "p__usecase_prepare_blank_tag_post__enter"
[] self = "/usecase/register_tag(post)" -> "p__usecase_register_tag_post__enter"
[] self = "Tail" -> "tail_wait"]
dummy_start(self) == /\ pc[self] = "dummy_start"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "Error"]
/\ UNCHANGED << steps, step, step_parameter, now,
responses, v_Accounts, v_Leads, v_Tags,
v_tag_ids, stack, dummy_input, lead,
account, input >>
dummy(self) == dummy_start(self)
salesforce_lead_post_(self) == /\ pc[self] = "salesforce_lead_post_"
/\ Assert(( lead[self] \in t_salesf_Lead ),
"Failure of assertion at line 614, column 8.")
/\ IF ~ValidLead( lead[self] )
THEN /\ responses' = [responses EXCEPT ![InterfaceOperation2ProcessName("/sf/lead(post)")] = InfrastructureServiceResponse( "status_404", Nil )]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ lead' = [lead EXCEPT ![self] = Head(stack[self]).lead]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
ELSE /\ pc' = [pc EXCEPT ![self] = "salesforce_lead_valid_input"]
/\ UNCHANGED << responses, stack,
lead >>
/\ UNCHANGED << steps, step, step_parameter,
now, v_Accounts, v_Leads,
v_Tags, v_tag_ids, dummy_input,
account, input >>
salesforce_lead_valid_input(self) == /\ pc[self] = "salesforce_lead_valid_input"
/\ v_Leads' = ({ entry \in v_Leads: entry.Id # lead[self].Id } \union { lead[self] })
/\ responses' = [responses EXCEPT ![InterfaceOperation2ProcessName("/sf/lead(post)")] = InfrastructureServiceResponse( "status_200", Nil )]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ lead' = [lead EXCEPT ![self] = Head(stack[self]).lead]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << steps, step,
step_parameter, now,
v_Accounts, v_Tags,
v_tag_ids, dummy_input,
account, input >>
salesforce_lead_post(self) == salesforce_lead_post_(self)
\/ salesforce_lead_valid_input(self)
salesforce_account_post_(self) == /\ pc[self] = "salesforce_account_post_"
/\ Assert(( account[self] \in t_salesf_Account ),
"Failure of assertion at line 639, column 8.")
/\ IF ~ValidAccount( account[self] )
THEN /\ responses' = [responses EXCEPT ![InterfaceOperation2ProcessName("/sf/account(post)")] = InfrastructureServiceResponse( "status_404", Nil )]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ account' = [account EXCEPT ![self] = Head(stack[self]).account]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
ELSE /\ pc' = [pc EXCEPT ![self] = "salesforce_account_valid_input"]
/\ UNCHANGED << responses, stack,
account >>
/\ UNCHANGED << steps, step, step_parameter,
now, v_Accounts, v_Leads,
v_Tags, v_tag_ids,
dummy_input, lead, input >>
salesforce_account_valid_input(self) == /\ pc[self] = "salesforce_account_valid_input"
/\ v_Accounts' = ({ entry \in v_Accounts: entry.Id # account[self].Id } \union { account[self] })
/\ responses' = [responses EXCEPT ![InterfaceOperation2ProcessName("/sf/account(post)")] = InfrastructureServiceResponse( "status_200", Nil )]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ account' = [account EXCEPT ![self] = Head(stack[self]).account]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << steps, step,
step_parameter, now,
v_Leads, v_Tags,
v_tag_ids, dummy_input,
lead, input >>
salesforce_account_post(self) == salesforce_account_post_(self)
\/ salesforce_account_valid_input(self)
petstore_prepare_blank_start(self) == /\ pc[self] = "petstore_prepare_blank_start"
/\ Assert(( Next_Tag_id \in v_tag_ids ),
"Failure of assertion at line 533, column 7 of macro called at line 661, column 9.")
/\ v_tag_ids' = v_tag_ids \ { Next_Tag_id }
/\ v_Tags' = (v_Tags \union {(New_Empty_Tag(Next_Tag_id))})
/\ pc' = [pc EXCEPT ![self] = "petstore_prepare_blank_done"]
/\ UNCHANGED << steps, step,
step_parameter, now,
responses, v_Accounts,
v_Leads, stack,
dummy_input, lead,
account, input >>
petstore_prepare_blank_done(self) == /\ pc[self] = "petstore_prepare_blank_done"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << steps, step,
step_parameter, now,
responses, v_Accounts,
v_Leads, v_Tags,
v_tag_ids, dummy_input,
lead, account, input >>
petstore_prepare_blank_tag(self) == petstore_prepare_blank_start(self)
\/ petstore_prepare_blank_done(self)
petstore_register_tag_start(self) == /\ pc[self] = "petstore_register_tag_start"
/\ PrintT(<< "input:", input[self] >>)
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "petstore_prepare_blank_tag",
pc |-> "petstore_register_tag_done" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "petstore_prepare_blank_start"]
/\ UNCHANGED << steps, step,
step_parameter, now,
responses, v_Accounts,
v_Leads, v_Tags,
v_tag_ids, dummy_input,
lead, account, input >>
petstore_register_tag_done(self) == /\ pc[self] = "petstore_register_tag_done"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ input' = [input EXCEPT ![self] = Head(stack[self]).input]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << steps, step,
step_parameter, now,
responses, v_Accounts,
v_Leads, v_Tags, v_tag_ids,
dummy_input, lead, account >>
petstore_register_tag(self) == petstore_register_tag_start(self)
\/ petstore_register_tag_done(self)
p__usecase_generate_lead_post__enter == /\ pc["/usecase/generate_lead(post)"] = "p__usecase_generate_lead_post__enter"
/\ ProcessEnabled( steps, "p__usecase_generate_lead_post_" )
/\ step' = ProcessRunning( steps )
/\ step_parameter' = ProcessParameter( steps )
/\ responses' = InfrastructureServiceInit
/\ now' = TickNext( now )
/\ \E _input \in { t \in ProcessParameterInput( t__usecase_generate_lead_post_ ) : ProcessParameterBind( t ) }:
/\ PrintT(<<"Default process p__usecase_generate_lead_post_ for operation '/usecase/generate_lead(post)',tick=", currentTime>>)
/\ Assert(( _input \in t__usecase_generate_lead_post_ ),
"Failure of assertion at line 698, column 13.")
/\ /\ lead' = [lead EXCEPT !["/usecase/generate_lead(post)"] = _input.lead]
/\ stack' = [stack EXCEPT !["/usecase/generate_lead(post)"] = << [ procedure |-> "salesforce_lead_post",
pc |-> "p__usecase_generate_lead_post__exit",
lead |-> lead["/usecase/generate_lead(post)"] ] >>
\o stack["/usecase/generate_lead(post)"]]
/\ pc' = [pc EXCEPT !["/usecase/generate_lead(post)"] = "salesforce_lead_post_"]
/\ UNCHANGED << steps, v_Accounts,
v_Leads, v_Tags,
v_tag_ids, dummy_input,
account, input >>
p__usecase_generate_lead_post__exit == /\ pc["/usecase/generate_lead(post)"] = "p__usecase_generate_lead_post__exit"
/\ steps' = ProcessesToRun( steps )
/\ pc' = [pc EXCEPT !["/usecase/generate_lead(post)"] = "p__usecase_generate_lead_post__enter"]
/\ UNCHANGED << step, step_parameter,
now, responses,
v_Accounts, v_Leads,
v_Tags, v_tag_ids,
stack, dummy_input,
lead, account, input >>
p__usecase_generate_lead_post_ == p__usecase_generate_lead_post__enter
\/ p__usecase_generate_lead_post__exit
p__usecase_create_account_post__enter == /\ pc["/usecase/create_account(post)"] = "p__usecase_create_account_post__enter"
/\ ProcessEnabled( steps, "p__usecase_create_account_post_" )
/\ step' = ProcessRunning( steps )
/\ step_parameter' = ProcessParameter( steps )
/\ responses' = InfrastructureServiceInit
/\ now' = TickNext( now )
/\ \E _input \in { t \in ProcessParameterInput( t__usecase_create_account_post_ ) : ProcessParameterBind( t ) }:
/\ PrintT(<<"Default process p__usecase_create_account_post_ for operation '/usecase/create_account(post)',tick=", currentTime>>)
/\ Assert(( _input \in t__usecase_create_account_post_ ),
"Failure of assertion at line 716, column 13.")
/\ /\ account' = [account EXCEPT !["/usecase/create_account(post)"] = _input.account]
/\ stack' = [stack EXCEPT !["/usecase/create_account(post)"] = << [ procedure |-> "salesforce_account_post",
pc |-> "p__usecase_create_account_post__exit",
account |-> account["/usecase/create_account(post)"] ] >>
\o stack["/usecase/create_account(post)"]]
/\ pc' = [pc EXCEPT !["/usecase/create_account(post)"] = "salesforce_account_post_"]
/\ UNCHANGED << steps, v_Accounts,
v_Leads, v_Tags,
v_tag_ids,
dummy_input, lead,
input >>
p__usecase_create_account_post__exit == /\ pc["/usecase/create_account(post)"] = "p__usecase_create_account_post__exit"
/\ steps' = ProcessesToRun( steps )
/\ pc' = [pc EXCEPT !["/usecase/create_account(post)"] = "p__usecase_create_account_post__enter"]
/\ UNCHANGED << step, step_parameter,
now, responses,
v_Accounts, v_Leads,
v_Tags, v_tag_ids,
stack, dummy_input,
lead, account, input >>
p__usecase_create_account_post_ == p__usecase_create_account_post__enter
\/ p__usecase_create_account_post__exit
p__usecase_prepare_blank_tag_post__enter == /\ pc["/usecase/prepare_blank_tag(post)"] = "p__usecase_prepare_blank_tag_post__enter"
/\ ProcessEnabled( steps, "p__usecase_prepare_blank_tag_post_" )
/\ step' = ProcessRunning( steps )
/\ step_parameter' = ProcessParameter( steps )
/\ responses' = InfrastructureServiceInit
/\ now' = TickNext( now )
/\ \E _input \in { t \in ProcessParameterInput( t__usecase_prepare_blank_tag_post_ ) : ProcessParameterBind( t ) }:
/\ PrintT(<<"Default process p__usecase_prepare_blank_tag_post_ for operation '/usecase/prepare_blank_tag(post)',tick=", currentTime>>)
/\ Assert(( _input.dummy = Nil ),
"Failure of assertion at line 735, column 14.")
/\ Assert(( _input = [ dummy |-> Nil ] ),
"Failure of assertion at line 567, column 7 of macro called at line 736, column 13.")
/\ stack' = [stack EXCEPT !["/usecase/prepare_blank_tag(post)"] = << [ procedure |-> "petstore_prepare_blank_tag",
pc |-> "p__usecase_prepare_blank_tag_post__exit" ] >>
\o stack["/usecase/prepare_blank_tag(post)"]]
/\ pc' = [pc EXCEPT !["/usecase/prepare_blank_tag(post)"] = "petstore_prepare_blank_start"]
/\ UNCHANGED << steps, v_Accounts,
v_Leads, v_Tags,
v_tag_ids,
dummy_input, lead,
account, input >>
p__usecase_prepare_blank_tag_post__exit == /\ pc["/usecase/prepare_blank_tag(post)"] = "p__usecase_prepare_blank_tag_post__exit"
/\ steps' = ProcessesToRun( steps )
/\ pc' = [pc EXCEPT !["/usecase/prepare_blank_tag(post)"] = "p__usecase_prepare_blank_tag_post__enter"]
/\ UNCHANGED << step,
step_parameter, now,
responses,
v_Accounts, v_Leads,
v_Tags, v_tag_ids,
stack, dummy_input,
lead, account,
input >>
p__usecase_prepare_blank_tag_post_ == p__usecase_prepare_blank_tag_post__enter
\/ p__usecase_prepare_blank_tag_post__exit
p__usecase_register_tag_post__enter == /\ pc["/usecase/register_tag(post)"] = "p__usecase_register_tag_post__enter"
/\ ProcessEnabled( steps, "p__usecase_register_tag_post_" )
/\ step' = ProcessRunning( steps )
/\ step_parameter' = ProcessParameter( steps )
/\ responses' = InfrastructureServiceInit
/\ now' = TickNext( now )
/\ \E _input \in { t \in ProcessParameterInput( t__usecase_register_tag_post_ ) : ProcessParameterBind( t ) }:
/\ PrintT(<<"Default process p__usecase_register_tag_post_ for operation '/usecase/register_tag(post)',tick=", currentTime>>)
/\ Assert(( _input \in t__usecase_register_tag_post_ ),
"Failure of assertion at line 753, column 13.")
/\ /\ input' = [input EXCEPT !["/usecase/register_tag(post)"] = _input]
/\ stack' = [stack EXCEPT !["/usecase/register_tag(post)"] = << [ procedure |-> "petstore_register_tag",
pc |-> "p__usecase_register_tag_post__exit",
input |-> input["/usecase/register_tag(post)"] ] >>
\o stack["/usecase/register_tag(post)"]]
/\ pc' = [pc EXCEPT !["/usecase/register_tag(post)"] = "petstore_register_tag_start"]
/\ UNCHANGED << steps, v_Accounts,
v_Leads, v_Tags,
v_tag_ids, dummy_input,
lead, account >>
p__usecase_register_tag_post__exit == /\ pc["/usecase/register_tag(post)"] = "p__usecase_register_tag_post__exit"
/\ steps' = ProcessesToRun( steps )
/\ pc' = [pc EXCEPT !["/usecase/register_tag(post)"] = "p__usecase_register_tag_post__enter"]
/\ UNCHANGED << step, step_parameter,
now, responses,
v_Accounts, v_Leads,
v_Tags, v_tag_ids, stack,
dummy_input, lead,
account, input >>
p__usecase_register_tag_post_ == p__usecase_register_tag_post__enter
\/ p__usecase_register_tag_post__exit
tail_wait == /\ pc["Tail"] = "tail_wait"
/\ ( Len(steps) = 0 )
/\ step' = "Tail"
/\ step_parameter' = {}
/\ pc' = [pc EXCEPT !["Tail"] = "tail_"]
/\ UNCHANGED << steps, now, responses, v_Accounts, v_Leads,
v_Tags, v_tag_ids, stack, dummy_input, lead,
account, input >>
tail_ == /\ pc["Tail"] = "tail_"
/\ TRUE
/\ pc' = [pc EXCEPT !["Tail"] = "tail_"]
/\ UNCHANGED << steps, step, step_parameter, now, responses,
v_Accounts, v_Leads, v_Tags, v_tag_ids, stack,
dummy_input, lead, account, input >>
tail == tail_wait \/ tail_
Next == p__usecase_generate_lead_post_ \/ p__usecase_create_account_post_
\/ p__usecase_prepare_blank_tag_post_ \/ p__usecase_register_tag_post_
\/ tail
\/ (\E self \in ProcSet: \/ dummy(self) \/ salesforce_lead_post(self)
\/ salesforce_account_post(self)
\/ petstore_prepare_blank_tag(self)
\/ petstore_register_tag(self))
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(p__usecase_generate_lead_post_)
/\ WF_vars(p__usecase_create_account_post_)
/\ WF_vars(p__usecase_prepare_blank_tag_post_)
/\ WF_vars(p__usecase_register_tag_post_)
/\ WF_vars(tail)
\* END TRANSLATION
(******************************************************************
Type invariants: Type constraint in specification
- modelData variables
- template state_type_invariant.mustache
******************************************************************)
(******************************************************************
Validate types for infrastructure service return values
- modelData infrastructureServices
- template state_type_invariant-infrastructure-service.mustache
******************************************************************)
(*
Type invariants for infrastructure service return values.
All fields in 'responses' state variable store a record [ status |-> ... , response |-> ... ]
*)
InfrastructureService_TypeInvariant__sf_lead_post_ == responses.p__sf_lead_post_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_account_post_ == responses.p__sf_account_post_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_account_get_ == responses.p__sf_account_get_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant__sf_lead_get_ == responses.p__sf_lead_get_.response \in { Nil }
\* Type invariant for infrastructure service return values
InfrastructureService_TypeInvariant == TRUE
/\ InfrastructureService_TypeInvariant__sf_lead_post_
/\ InfrastructureService_TypeInvariant__sf_account_post_
/\ InfrastructureService_TypeInvariant__sf_account_get_
/\ InfrastructureService_TypeInvariant__sf_lead_get_
(*
Extension point for specification invariants
- modelData none
- template extend/extend_invariant.mustache
*)
\* Operators for correctness
\* Type constraints
Leads_TypeInvariant == \A entry \in v_Leads: entry \in t_salesf_Lead
Account_TypeInvariant == \A entry \in v_Accounts: entry \in t_salesf_Account
Tag_TypeInvariant == \A entry \in v_Tags: entry \in t_Tag
\* Correcness criteria
\* All entries in state variable 'v_Leads' are 'ValidLead'
Correctness_lead_valid == \A entry \in v_Leads: ValidLead( entry )
\* All entries in 'v_Leads' have unique 'id'
Correctness_lead_unique == \A lead1 \in v_Leads: \A lead2 \in v_Leads: lead1.Id = lead2.Id => lead1 = lead2
\* Combine all correcness criteria on 'Lead', this operator confiugered as INVARIANT
Correctness_lead ==
Correctness_lead_valid
/\ Correctness_lead_unique
\* All entries in state variable 'v_Accounts' are 'ValidAccount'
Correctness_account_valid == \A entry \in v_Accounts: ValidAccount( entry )
\* All entries in 'v_Accounts' have unique 'id'
Correctness_account_unique == \A account1 \in v_Accounts: \A account2 \in v_Accounts: account1.Id = account2.Id => account1 = account2
\* Combine all correcness criteria on 'Account', this operator confiugered as INVARIANT
Correctness_account ==
Correctness_account_valid
/\ Correctness_account_unique
\* Operators for possibilities
(*
Define an operator 'at_least_two_tags' to check that
at least two entries are found in state variable 'v_tags'.
*)
at_least_two_leads == Cardinality( v_Leads ) > 1
(*
Possibility operator to check that at least two entries are found
in state variable 'v_Tags'.
*)
at_least_two_tags == Cardinality( v_Tags ) > 1
at_least_two_accounts == Cardinality( v_Accounts ) > 1
(*
Extension point for assumptions
- modelData none
- template extend/extend_assumptions.mustache
*)
(* ******************************************************************
Helpers to make assumptions
******************************************************************)
(*
True iff in all records in 'set' have 'field' type 'domain'
Cannot evaluate 'p \in set' if set contains too many elements
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in set } = domain
Attempted to construct a set with too many elements (>1000000).
Assume_CorrectDomain( set, field, domain ) == (CHOOSE x \in set : TRUE)[field] \in domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == set[field] = domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == DOMAIN set[field] = domain
A non-function (a set of the form [d1 : S1, ... , dN : SN]) was applied as a function.
Assume_CorrectDomain( set, field, domain ) == (CHOOSE x \in set[field] : TRUE) \in domain
Overflow when computing the number of elements in:
Assume_CorrectDomain( set, field, domain ) == IF Cardinality( set ) > 100
THEN Print( << "Set cardinality exceeded ", Cardinality( set ), " continue" >>, TRUE )
ELSE { p[field] : p \in set } = domain
*)
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
Assume_CorrectDomain( set, field, domain ) == { p[field] : p \in set } = domain
Assume_salesf_Lead_Domains ==
Assume_CorrectDomain( t_salesf_Lead, "Id", d_lead_id )
/\ Assume_CorrectDomain( t_salesf_Lead, "Name", d_name )
/\ Assume_CorrectDomain( t_salesf_Lead, "Street", d_street )
/\ Assume_CorrectDomain( t_salesf_Lead, "City", d_city )
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
ASSUME Assume_salesf_Lead_Domains
Assume_salesf_Account_Domains ==
Assume_CorrectDomain( t_salesf_Account, "Id", d_account_id )
/\ Assume_CorrectDomain( t_salesf_Account, "Name", d_name )
/\ Assume_CorrectDomain( t_salesf_Account, "Street", d_street )
/\ Assume_CorrectDomain( t_salesf_Account, "City", d_city )
\* FIXME: error with too many elements in 'Assume_CorrectDomain'
\* ASSUME Assume_salesf_Account_Domains
Assume_Lead_Domains ==
Assume_CorrectDomain( t_Lead, "id", d_lead_id )
ASSUME Assume_Lead_Domains
Assume_Tag_Domains ==
Assume_CorrectDomain( t_Tag, "id", d_tag_id )
ASSUME Assume_Tag_Domains
Assume_Address_Domains ==
Assume_CorrectDomain( t_Address, "street", d_street )
/\ Assume_CorrectDomain( t_Address, "city", d_city )
ASSUME Assume_Address_Domains
Assume_Owner_Domains ==
Assume_CorrectDomain( t_Owner, "name", d_name )
ASSUME Assume_Owner_Domains
=============================================================================
Raw
possible_at_least_two_leads.cfg
(*
Model version: 0.0.1-SNAPSHOT
Generator version: 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
*)
\* Configuration taken from uc1/setup.cfg
\* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
\* Start here
(*
Model version: 0.0.1-SNAPSHOT
Generator version 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
*)
SPECIFICATION Spec
\* Add statements after this line.
(* Environment *)
CONSTANT Steps <- RunSteps
(* 'enabled' macro check is process enables *)
CONSTANT ProcessEnabled <- RunProcessEnabled
CONSTANT ProcessRunning <- RunProcessRunning
CONSTANT ProcessParameter <- RunProcessParameter
CONSTANT ProcessesToRun <- RunProcessesToRun
CONSTANT TickNext <- RunTickNext
(* Declare magic constants *)
CONSTANT WildCard = WildCard
CONSTANT Nil = Nil
(* Pluscal sets 'defaultInitValue' for unitialized variables *)
CONSTANT defaultInitValue <- Nil
(******************************************************************
Map domain ranges in setup to specification domains:
Configure specification domains
- modelData domains
- template domains_assign.mustache
******************************************************************)
CONSTANT d_name <- Run_d_name
CONSTANT d_street <- Run_d_street
CONSTANT d_city <- Run_d_city
CONSTANT d_lead_id <- Run_d_lead_id
CONSTANT d_not_used <- Run_d_not_used
CONSTANT d_account_id <- Run_d_account_id
CONSTANT d_tag_id <- Run_d_tag_id
CONSTANT d_default_domain <- Run_d_default_domain
(******************************************************************
Activate Type invariants: Activate specification invariants
- modelData variables
- template state_type_invariant_cfg.mustache
******************************************************************)
\* Ensure that infrastrucutre services return correct types
INVARIANT InfrastructureService_TypeInvariant
(*
Extension point to activate specification invariants - DEPRECATED
- modelData none
- template extend/extend_invariant_cfg.mustache
*)
(******************************************************************
Activate Type invariants: Activate invariants defined in sbuilder.yaml
- modelData invariants
- template invariant_activate.mustache
******************************************************************)
INVARIANT Correctness_lead_valid
INVARIANT Correctness_lead_unique
INVARIANT Leads_TypeInvariant
INVARIANT Tag_TypeInvariant
INVARIANT Account_TypeInvariant
INVARIANT Correctness_account
\* End here
\* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
PROPERTY possible_at_least_two_leads
Raw
possible_at_least_two_leads.tla
Model version: 0.0.1-SNAPSHOT
Generator version: 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
------------------------------ MODULE possible_at_least_two_leads ------------------------------
EXTENDS setup
(*
Define possibility for operator at_least_two_leads
We require that possible_at_least_two_leads is false allways.
Interpreat violation of this property that it is possible
to reach a state where the property holds.
*)
possible_at_least_two_leads == [] ~at_least_two_leads
=============================================================================
Raw
setup.cfg
(*
Model version: 0.0.1-SNAPSHOT
Generator version 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
*)
SPECIFICATION Spec
\* Add statements after this line.
(* Environment *)
CONSTANT Steps <- RunSteps
(* 'enabled' macro check is process enables *)
CONSTANT ProcessEnabled <- RunProcessEnabled
CONSTANT ProcessRunning <- RunProcessRunning
CONSTANT ProcessParameter <- RunProcessParameter
CONSTANT ProcessesToRun <- RunProcessesToRun
CONSTANT TickNext <- RunTickNext
(* Declare magic constants *)
CONSTANT WildCard = WildCard
CONSTANT Nil = Nil
(* Pluscal sets 'defaultInitValue' for unitialized variables *)
CONSTANT defaultInitValue <- Nil
(******************************************************************
Map domain ranges in setup to specification domains:
Configure specification domains
- modelData domains
- template domains_assign.mustache
******************************************************************)
CONSTANT d_name <- Run_d_name
CONSTANT d_street <- Run_d_street
CONSTANT d_city <- Run_d_city
CONSTANT d_lead_id <- Run_d_lead_id
CONSTANT d_not_used <- Run_d_not_used
CONSTANT d_account_id <- Run_d_account_id
CONSTANT d_tag_id <- Run_d_tag_id
CONSTANT d_default_domain <- Run_d_default_domain
(******************************************************************
Activate Type invariants: Activate specification invariants
- modelData variables
- template state_type_invariant_cfg.mustache
******************************************************************)
\* Ensure that infrastrucutre services return correct types
INVARIANT InfrastructureService_TypeInvariant
(*
Extension point to activate specification invariants - DEPRECATED
- modelData none
- template extend/extend_invariant_cfg.mustache
*)
(******************************************************************
Activate Type invariants: Activate invariants defined in sbuilder.yaml
- modelData invariants
- template invariant_activate.mustache
******************************************************************)
INVARIANT Correctness_lead_valid
INVARIANT Correctness_lead_unique
INVARIANT Leads_TypeInvariant
INVARIANT Tag_TypeInvariant
INVARIANT Account_TypeInvariant
INVARIANT Correctness_account
Raw
setup.tla
Model version: 0.0.1-SNAPSHOT
Generator version: 0.1.1-SNAPSHOT
Generation timestemp: 2016-04-25 11:22:06
------------------------------ MODULE setup ------------------------------
EXTENDS model, TLC
(* Control execution *)
\* RunProcessRunning( stepdefs ) == { e.process : e \in Head( stepdefs ) }
RunProcessRunning( stepdefs ) == (CHOOSE s \in Head( stepdefs ): TRUE ).process
RunProcessEnabled( stepdefs, s ) == Len( stepdefs ) # 0 /\ s = RunProcessRunning( stepdefs )
RunProcessesToRun( stepdefs ) == Tail( stepdefs )
RunProcessParameter( stepdefs ) == Head( stepdefs )
RunTickNext( t ) == t + 1
(******************************************************************
Assign values to skeleton domains: Setup domain values
- modelData domains
- template domains_run.mustache
*******************************************************************)
(* Domains for uc1 start *)
Run_d_name == { "d_name_1", "d_name_2" } \cup {Nil} \*
Run_d_street == { "d_street_1" } \cup {Nil} \*
Run_d_city == { "d_city_1" } \cup {Nil} \*
Run_d_lead_id == { "d_lead_id_1", "d_lead_id_2" } \cup {Nil} \*
Run_d_not_used == { "d_not_used_1" } \cup {Nil} \*
Run_d_account_id == { "d_account_id_1" } \cup {Nil} \*
Run_d_tag_id == { "d_tag_id_1" } \cup {Nil} \*
Run_d_default_domain == { "d_default_domain_1" } \cup {Nil} \*
(* Domains for uc1 end *)
(******************************************************************
Environment model running the steps
Setup environment execution steps
- modelData steps
- template setup/steps_run.mustache
******************************************************************)
RunSteps == <<
{ [ process |-> "p__usecase_generate_lead_post_",
bindRule |-> WildCard
,
bindSet |-> { [ lead |-> [ Id |-> "d_lead_id_1", IsDeleted |-> "d_not_used_1", MasterRecordId |-> "d_not_used_1", LastName |-> "d_not_used_1", FirstName |-> "d_not_used_1", Salutation |-> "d_not_used_1", Name |-> "d_name_1", Title |-> "d_not_used_1", Company |-> "d_not_used_1", Street |-> "d_street_1", City |-> "d_city_1", State |-> "d_not_used_1", PostalCode |-> "d_not_used_1", Country |-> "d_not_used_1", Latitude |-> "d_not_used_1", Longitude |-> "d_not_used_1", Address |-> "d_not_used_1", Phone |-> "d_not_used_1", MobilePhone |-> "d_not_used_1", Fax |-> "d_not_used_1", Email |-> "d_not_used_1", Website |-> "d_not_used_1", PhotoUrl |-> "d_not_used_1", Description |-> "d_not_used_1", LeadSource |-> "d_not_used_1", Status |-> "d_not_used_1", Industry |-> "d_not_used_1", Rating |-> "d_not_used_1", AnnualRevenue |-> "d_not_used_1", NumberOfEmployees |-> "d_not_used_1", OwnerId |-> "d_not_used_1", IsConverted |-> "d_not_used_1", ConvertedDate |-> "d_not_used_1", ConvertedAccountId |-> "d_not_used_1", ConvertedContactId |-> "d_not_used_1", ConvertedOpportunityId |-> "d_not_used_1", IsUnreadByOwner |-> "d_not_used_1", CreatedDate |-> "d_not_used_1", CreatedById |-> "d_not_used_1", LastModifiedDate |-> "d_not_used_1", LastModifiedById |-> "d_not_used_1", SystemModstamp |-> "d_not_used_1", LastActivityDate |-> "d_not_used_1", LastViewedDate |-> "d_not_used_1", LastReferencedDate |-> "d_not_used_1", Jigsaw |-> "d_not_used_1", JigsawContactId |-> "d_not_used_1", CleanStatus |-> "d_not_used_1", CompanyDunsNumber |-> "d_not_used_1", DandbCompanyId |-> "d_not_used_1", EmailBouncedReason |-> "d_not_used_1", EmailBouncedDate |-> "d_not_used_1", SICCode__c |-> "d_not_used_1", ProductInterest__c |-> "d_not_used_1", Primary__c |-> "d_not_used_1", CurrentGenerators__c |-> "d_not_used_1", NumberofLocations__c |-> "d_not_used_1", pet_tag__c |-> "d_not_used_1"
]
] }
]
} , (* interface/process : _usecase_generate_lead_post_ *)
{ [ process |-> "p__usecase_generate_lead_post_",
bindRule |-> WildCard
,
bindSet |-> { [ lead |-> [ Name |-> "d_name_2", Id |-> "d_lead_id_2", IsDeleted |-> "d_not_used_1", MasterRecordId |-> "d_not_used_1", LastName |-> "d_not_used_1", FirstName |-> "d_not_used_1", Salutation |-> "d_not_used_1", Title |-> "d_not_used_1", Company |-> "d_not_used_1", Street |-> "d_street_1", City |-> "d_city_1", State |-> "d_not_used_1", PostalCode |-> "d_not_used_1", Country |-> "d_not_used_1", Latitude |-> "d_not_used_1", Longitude |-> "d_not_used_1", Address |-> "d_not_used_1", Phone |-> "d_not_used_1", MobilePhone |-> "d_not_used_1", Fax |-> "d_not_used_1", Email |-> "d_not_used_1", Website |-> "d_not_used_1", PhotoUrl |-> "d_not_used_1", Description |-> "d_not_used_1", LeadSource |-> "d_not_used_1", Status |-> "d_not_used_1", Industry |-> "d_not_used_1", Rating |-> "d_not_used_1", AnnualRevenue |-> "d_not_used_1", NumberOfEmployees |-> "d_not_used_1", OwnerId |-> "d_not_used_1", IsConverted |-> "d_not_used_1", ConvertedDate |-> "d_not_used_1", ConvertedAccountId |-> "d_not_used_1", ConvertedContactId |-> "d_not_used_1", ConvertedOpportunityId |-> "d_not_used_1", IsUnreadByOwner |-> "d_not_used_1", CreatedDate |-> "d_not_used_1", CreatedById |-> "d_not_used_1", LastModifiedDate |-> "d_not_used_1", LastModifiedById |-> "d_not_used_1", SystemModstamp |-> "d_not_used_1", LastActivityDate |-> "d_not_used_1", LastViewedDate |-> "d_not_used_1", LastReferencedDate |-> "d_not_used_1", Jigsaw |-> "d_not_used_1", JigsawContactId |-> "d_not_used_1", CleanStatus |-> "d_not_used_1", CompanyDunsNumber |-> "d_not_used_1", DandbCompanyId |-> "d_not_used_1", EmailBouncedReason |-> "d_not_used_1", EmailBouncedDate |-> "d_not_used_1", SICCode__c |-> "d_not_used_1", ProductInterest__c |-> "d_not_used_1", Primary__c |-> "d_not_used_1", CurrentGenerators__c |-> "d_not_used_1", NumberofLocations__c |-> "d_not_used_1", pet_tag__c |-> "d_not_used_1"
]
] }
]
} , (* interface/process : _usecase_generate_lead_post_ *)
{ [ process |-> "p__usecase_generate_lead_post_",
bindRule |-> WildCard
,
bindSet |-> { [ lead |-> [ Id |-> "d_lead_id_2", IsDeleted |-> "d_not_used_1", MasterRecordId |-> "d_not_used_1", LastName |-> "d_not_used_1", FirstName |-> "d_not_used_1", Salutation |-> "d_not_used_1", Name |-> "d_name_1", Title |-> "d_not_used_1", Company |-> "d_not_used_1", Street |-> "d_street_1", City |-> "d_city_1", State |-> "d_not_used_1", PostalCode |-> "d_not_used_1", Country |-> "d_not_used_1", Latitude |-> "d_not_used_1", Longitude |-> "d_not_used_1", Address |-> "d_not_used_1", Phone |-> "d_not_used_1", MobilePhone |-> "d_not_used_1", Fax |-> "d_not_used_1", Email |-> "d_not_used_1", Website |-> "d_not_used_1", PhotoUrl |-> "d_not_used_1", Description |-> "d_not_used_1", LeadSource |-> "d_not_used_1", Status |-> "d_not_used_1", Industry |-> "d_not_used_1", Rating |-> "d_not_used_1", AnnualRevenue |-> "d_not_used_1", NumberOfEmployees |-> "d_not_used_1", OwnerId |-> "d_not_used_1", IsConverted |-> "d_not_used_1", ConvertedDate |-> "d_not_used_1", ConvertedAccountId |-> "d_not_used_1", ConvertedContactId |-> "d_not_used_1", ConvertedOpportunityId |-> "d_not_used_1", IsUnreadByOwner |-> "d_not_used_1", CreatedDate |-> "d_not_used_1", CreatedById |-> "d_not_used_1", LastModifiedDate |-> "d_not_used_1", LastModifiedById |-> "d_not_used_1", SystemModstamp |-> "d_not_used_1", LastActivityDate |-> "d_not_used_1", LastViewedDate |-> "d_not_used_1", LastReferencedDate |-> "d_not_used_1", Jigsaw |-> "d_not_used_1", JigsawContactId |-> "d_not_used_1", CleanStatus |-> "d_not_used_1", CompanyDunsNumber |-> "d_not_used_1", DandbCompanyId |-> "d_not_used_1", EmailBouncedReason |-> "d_not_used_1", EmailBouncedDate |-> "d_not_used_1", SICCode__c |-> "d_not_used_1", ProductInterest__c |-> "d_not_used_1", Primary__c |-> "d_not_used_1", CurrentGenerators__c |-> "d_not_used_1", NumberofLocations__c |-> "d_not_used_1", pet_tag__c |-> "d_not_used_1"
]
] }
]
} , (* interface/process : _usecase_generate_lead_post_ *)
{ [ process |-> "p__usecase_generate_lead_post_",
bindRule |-> WildCard
,
bindSet |-> { [ lead |-> [ Id |-> Nil, IsDeleted |-> Nil, MasterRecordId |-> Nil, LastName |-> Nil, FirstName |-> Nil, Salutation |-> Nil, Name |-> Nil, Title |-> Nil, Company |-> Nil, Street |-> Nil, City |-> Nil, State |-> Nil, PostalCode |-> Nil, Country |-> Nil, Latitude |-> Nil, Longitude |-> Nil, Address |-> Nil, Phone |-> Nil, MobilePhone |-> Nil, Fax |-> Nil, Email |-> Nil, Website |-> Nil, PhotoUrl |-> Nil, Description |-> Nil, LeadSource |-> Nil, Status |-> Nil, Industry |-> Nil, Rating |-> Nil, AnnualRevenue |-> Nil, NumberOfEmployees |-> Nil, OwnerId |-> Nil, IsConverted |-> Nil, ConvertedDate |-> Nil, ConvertedAccountId |-> Nil, ConvertedContactId |-> Nil, ConvertedOpportunityId |-> Nil, IsUnreadByOwner |-> Nil, CreatedDate |-> Nil, CreatedById |-> Nil, LastModifiedDate |-> Nil, LastModifiedById |-> Nil, SystemModstamp |-> Nil, LastActivityDate |-> Nil, LastViewedDate |-> Nil, LastReferencedDate |-> Nil, Jigsaw |-> Nil, JigsawContactId |-> Nil, CleanStatus |-> Nil, CompanyDunsNumber |-> Nil, DandbCompanyId |-> Nil, EmailBouncedReason |-> Nil, EmailBouncedDate |-> Nil, SICCode__c |-> Nil, ProductInterest__c |-> Nil, Primary__c |-> Nil, CurrentGenerators__c |-> Nil, NumberofLocations__c |-> Nil, pet_tag__c |-> Nil
]
] }
]
} , (* interface/process : _usecase_generate_lead_post_ *)
{ [ process |-> "p__usecase_generate_lead_post_",
bindRule |-> WildCard
,
bindSet |-> { [ lead |-> [ Id |-> "d_lead_id_2", IsDeleted |-> Nil, MasterRecordId |-> Nil, LastName |-> Nil, FirstName |-> Nil, Salutation |-> Nil, Name |-> Nil, Title |-> Nil, Company |-> Nil, Street |-> Nil, City |-> Nil, State |-> Nil, PostalCode |-> Nil, Country |-> Nil, Latitude |-> Nil, Longitude |-> Nil, Address |-> Nil, Phone |-> Nil, MobilePhone |-> Nil, Fax |-> Nil, Email |-> Nil, Website |-> Nil, PhotoUrl |-> Nil, Description |-> Nil, LeadSource |-> Nil, Status |-> Nil, Industry |-> Nil, Rating |-> Nil, AnnualRevenue |-> Nil, NumberOfEmployees |-> Nil, OwnerId |-> Nil, IsConverted |-> Nil, ConvertedDate |-> Nil, ConvertedAccountId |-> Nil, ConvertedContactId |-> Nil, ConvertedOpportunityId |-> Nil, IsUnreadByOwner |-> Nil, CreatedDate |-> Nil, CreatedById |-> Nil, LastModifiedDate |-> Nil, LastModifiedById |-> Nil, SystemModstamp |-> Nil, LastActivityDate |-> Nil, LastViewedDate |-> Nil, LastReferencedDate |-> Nil, Jigsaw |-> Nil, JigsawContactId |-> Nil, CleanStatus |-> Nil, CompanyDunsNumber |-> Nil, DandbCompanyId |-> Nil, EmailBouncedReason |-> Nil, EmailBouncedDate |-> Nil, SICCode__c |-> Nil, ProductInterest__c |-> Nil, Primary__c |-> Nil, CurrentGenerators__c |-> Nil, NumberofLocations__c |-> Nil, pet_tag__c |-> Nil
]
] }
]
} (* interface/process : _usecase_generate_lead_post_ *)
>>
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment